1 % (c) 2022-2026 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(pathes_lib, [lib_component_full_path/4,
6 lib_component_available/6,
7 check_lib_component_available/1,
8 unavailable_extension/2,
9 available_extension/1,
10 check_lib_contents/2, check_lib_contents/3,
11 install_lib_component/2,
12 safe_load_foreign_resource/2]).
13
14 % TO DO: interface with lib_component_implements_extension/2
15
16
17 :- use_module(module_information,[module_info/2]).
18 :- module_info(group,typechecker).
19 :- module_info(description,'This module checks the contents of the lib folder and can install some missing components').
20
21 :- use_module(library(file_systems)).
22 :- use_module(library(system)).
23 :- use_module(library(lists)).
24 :- use_module(pathes, [runtime_application_path/1]).
25 :- use_module(pathes_extensions_db, [compile_time_unavailable_extension/2,
26 prob_extension/1, lib_component_implements_extension/4, lib_file_suffix/3]).
27 :- use_module(tools_platform, [host_platform/1, host_processor/1]).
28 :- use_module(tools_printing,[format_with_colour_nl/4]).
29 :- use_module(error_manager).
30 :- use_module(preferences, [get_preference/2]).
31 :- use_module(probsrc(tools_strings),[ajoin/2, ajoin_with_sep/3]).
32 :- use_module(system_call).
33 :- use_module(debug,[debug_format/3]).
34
35 % The predicates in this module can only be called at runtime,
36 % because they check whether certain files are present in the lib directory.
37 % For compile-time checks,
38 % use compile_time_unavailable_extension/2 from the pathes_extensions_db module instead
39 % (possibly with an additional runtime check).
40
41 add_file_suffix(Name,Kind,FullFile) :-
42 host_platform(Platform),
43 lib_file_suffix(Kind,Platform,Suffix),
44 atom_concat(Name,Suffix,FullFile).
45
46 lib_component_full_path(executable,Name,ltsmin_extension,FullFile) :-
47 !,
48 get_preference(path_to_ltsmin,LTSMinRel),
49 runtime_application_path(ProBHome),
50 absolute_file_name(LTSMinRel,LTSMinAbs,[relative_to(ProBHome)]),
51 add_file_suffix(Name,executable,File),
52 absolute_file_name(File,FullFile,[relative_to(LTSMinAbs)]).
53 lib_component_full_path(Kind,Name,_,FullFile) :-
54 add_file_suffix(Name,Kind,File),
55 absolute_file_name(prob_lib(File),FullFile).
56
57 check_lib_component_available(Component) :-
58 lib_component_available(Component,_Kind,_Name,FullFile,_ProBExtension,Available),
59 (Available=true
60 -> add_message(Component,'File for component is available: ',FullFile)
61 ; add_warning(Component,'File for component does not exist: ',FullFile)
62 ).
63
64 lib_component_available(C,Kind,Name,FullFile,ProBExtension,Available) :-
65 ? lib_component_implements_extension(C,Kind,Name,ProBExtension),
66 lib_component_full_path(Kind,Name,ProBExtension,FullFile),
67 (file_exists(FullFile) -> Available=true ; Available=false).
68
69 unavailable_extension(E, Reason) :- compile_time_unavailable_extension(E, Reason), !.
70 unavailable_extension(E, Reason) :-
71 ? lib_component_available(_Component, _Kind, _Name, FullFile, E, false),
72 atom_concat('required file missing: ', FullFile, Reason).
73
74 available_extension(E) :-
75 prob_extension(E),
76 \+ unavailable_extension(E,_).
77
78 prob_lib_folder(F) :- absolute_file_name(prob_lib('/'),F).
79
80 check_lib_contents(Stream,Verbose) :-
81 check_lib_contents(Stream,_,Verbose).
82 check_lib_contents(Stream,Comp,Verbose) :-
83 prob_lib_folder(FF),
84 (Verbose=silent -> true ; format_with_colour_nl(Stream,[blue],'Checking contents of lib folder: ~w',[FF])),
85 lib_component_available(Comp,Kind,_Name,_FullFile,ProBExtension,Available),
86 (Available=true
87 -> (Verbose=verbose -> format_with_colour_nl(Stream,[green],'~w (~w) found',[Comp,Kind])
88 ; true
89 )
90 ; format_with_colour_nl(Stream,[red],'~w (~w) not found, ~w not available',[Comp,Kind,ProBExtension]),
91 format_with_colour_nl(Stream,[blue],' * to install component run: probcli --install ~w~n',[Comp])
92 ),
93 fail.
94 check_lib_contents(_,_,_).
95
96
97 % url(Component,Platform,Processor,URL,File,Kind)
98 url(ltsmin,linux,_,
99 'https://github.com/utwente-fmt/ltsmin/releases/download/v3.0.2/','ltsmin-v3.0.2-linux.tgz',tgz).
100 url(ltsmin,darwin,_, % these are Intel binaries; but they run under Rosetta
101 'https://github.com/utwente-fmt/ltsmin/releases/download/v3.0.2/','ltsmin-v3.0.2-osx.tgz',tgz).
102
103 url(ltl2ba,linux,x86_64,'https://stups.hhu-hosting.de/downloads/ltl2ba_pl/sicstus4.9/linux-x86_64/','ltl2ba.so',bundle).
104 url(ltl2ba,darwin,_,'https://stups.hhu-hosting.de/downloads/ltl2ba_pl/sicstus4.9/macos/','ltl2ba.bundle',bundle).
105 url(ltl2ba,windows,x86_64,'https://stups.hhu-hosting.de/downloads/ltl2ba_pl/sicstus4.9/windows-x86_64/','ltl2ba.dll',bundle).
106 url(setlog,_,_,'https://stups.hhu-hosting.de/downloads/setlog_wrapper/','setlog-cli.qlf',qlf).
107 url(z3,darwin,aarch64,Z3,'z3-5.0.0-arm64-osx-13.3.zip',
108 zip('z3-5.0.0-arm64-osx-13.3/bin/libz3.dylib')) :- z3_url(Z3).
109 url(z3,darwin,x86_64,Z3,'z3-5.0.0-x64-osx-13.3.zip',
110 zip('z3-5.0.0-x64-osx-13.3/bin/libz3.dylib')) :- z3_url(Z3).
111 url(z3,windows,x86_64,Z3,'z3-5.0.0-x64-win.zip', % libz3.dll needs the C++ runtime of Visual Studio, which is included
112 zip(['z3-5.0.0-x64-win/bin/libz3.dll','z3-5.0.0-x64-win/bin/msvcp140.dll',
113 'z3-5.0.0-x64-win/bin/vcruntime140.dll','z3-5.0.0-x64-win/bin/vcruntime140_1.dll'])) :- z3_url(Z3).
114 url(z3,linux,x86_64,Z3,'z3-5.0.0-x64-glibc-2.39.zip', % requires glibc 2.38 or later
115 zip('z3-5.0.0-x64-glibc-2.39/bin/libz3.so')) :- z3_url(Z3).
116 url(z3,linux,aarch64,Z3,'z3-5.0.0-arm64-glibc-2.38.zip',
117 zip('z3-5.0.0-arm64-glibc-2.38/bin/libz3.so')) :- z3_url(Z3).
118
119 % the shared cvc5 releases contain libcvc5 and the libraries it depends on (libpoly, GMP, MPFR) in their lib folder
120 url(cvc5,darwin,aarch64,URL,'cvc5-macOS-arm64-shared.zip',zip(Files)) :-
121 cvc5_url(URL), cvc5_libs(darwin,'cvc5-macOS-arm64-shared/lib/',Files).
122 url(cvc5,darwin,x86_64,URL,'cvc5-macOS-x86_64-shared.zip',zip(Files)) :-
123 cvc5_url(URL), cvc5_libs(darwin,'cvc5-macOS-x86_64-shared/lib/',Files).
124 url(cvc5,linux,x86_64,URL,'cvc5-Linux-x86_64-shared.zip',zip(Files)) :- % requires glibc 2.33 or later
125 cvc5_url(URL), cvc5_libs(linux,'cvc5-Linux-x86_64-shared/lib/',Files).
126 url(cvc5,linux,aarch64,URL,'cvc5-Linux-arm64-shared.zip',zip(Files)) :-
127 cvc5_url(URL), cvc5_libs(linux,'cvc5-Linux-arm64-shared/lib/',Files).
128
129 z3_url('https://github.com/Z3Prover/z3/releases/download/z3-5.0.0/').
130 cvc5_url('https://github.com/cvc5/cvc5/releases/download/cvc5-1.4.1/').
131
132 % cvc5_libs(Platform,FolderInZip,Files): the libraries to extract, named as the extension refers to them
133 % (the install names on macOS, the SONAMEs on Linux)
134 cvc5_libs(Platform,Folder,Files) :-
135 cvc5_lib_names(Platform,Names),
136 prefix_atoms(Names,Folder,Files).
137
138 cvc5_lib_names(darwin,['libcvc5.1.dylib','libpoly.0.dylib','libpolyxx.0.dylib','libmpfr.6.dylib','libgmp.10.dylib']).
139 cvc5_lib_names(linux,['libcvc5.so.1','libpoly.so.0','libpolyxx.so.0','libmpfr.so.6','libgmp.so.10']).
140 % Note: no Windoes rules for cvc5, because DLL built against LLVM's libc++ not compatible with MinGW build
141
142 prefix_atoms([],_,[]).
143 prefix_atoms([Name|T],Prefix,[File|FT]) :- atom_concat(Prefix,Name,File), prefix_atoms(T,Prefix,FT).
144 %ltsmin_url('https://github.com/utwente-fmt/ltsmin/releases').
145
146 url7(Component,Plat,Proc,URL,File,Localfile,Kind) :- Localfile=File,
147 url(Component,Plat,Proc,URL,File,Kind).
148 url7(plantuml,_,_,'https://github.com/plantuml/plantuml/releases/download/v1.2024.8/','plantuml-epl-1.2024.8.jar','plantuml.jar',jar).
149
150 % curl -L https://github.com/utwente-fmt/ltsmin/releases/download/v3.0.2/ltsmin-v3.0.2-osx.tgz -o ~/Desktop/ltsmin-v3.0.2-osx.tgz
151
152 install_lib_component(Component,Opts) :-
153 host_platform(Plat),
154 host_processor(Proc),
155 url7(Component,Plat,Proc,URL,File,Localfile,Kind),!,
156 install_lib_component_aux(Component,URL,File,Localfile,Kind,Opts).
157 install_lib_component(Component,_) :-
158 host_platform(Plat),
159 host_processor(Proc),
160 url(Component,Plat,RProc,_,_,_), % we know the component and there are rules
161 Proc \= RProc,!, % but not for this processor
162 add_error(install_lib_component,'No rules to install for this processor:',Component).
163 install_lib_component(Component,_) :-
164 host_platform(Plat),
165 url(Component,RPlat,_,_,_,_), % we know the component and there are rules
166 Plat \= RPlat,!, % but not for this platform
167 add_error(install_lib_component,'No rules to install on this platform:',Component).
168 install_lib_component(Component,_) :-
169 add_error(install_lib_component,'Unknown component, no rules to install:',Component).
170
171
172 install_lib_component_aux(Component,URL,File,Localfile,Kind,Opts) :-
173 (member(silent,Opts) -> true
174 ; format_with_colour_nl(user_output,[blue],'Installing component ~w from ~w',[Component,URL])),
175 ajoin([URL,File],FullURL),
176 absolute_file_name(prob_lib(Localfile),LocalLibFile),
177 my_system_call('curl',['-L',FullURL,'-o',LocalLibFile],Opts), % will not work on Windows
178 % TODO: we could use curl -I FullURL to detect if file exists; we should get HTTP/1.1 200 OK
179 prob_lib_folder(LibFolder),
180 complete_installation(Component,LibFolder,LocalLibFile,Kind,Opts),
181 !,
182 (member(dryrun,Opts) -> true ; format_with_colour_nl(user_output,green,'Installation complete',[])).
183 install_lib_component_aux(Component,_,_,_,_,_) :-
184 add_error(install_lib_component,'Installation of component failed:',Component).
185
186 % perform steps after downloading file
187 complete_installation(ltsmin,LibFolder,LocalLibFile,_,Opts) :- !,
188 my_system_call('tar',['-xvzf',LocalLibFile,'-C',LibFolder],Opts), % creates v3.0.2 folder
189 ajoin([LibFolder,'/v3.0.2/bin'],LTSMinFolder),
190 move_file(LTSMinFolder,LibFolder,'prob2lts-seq',Opts),
191 move_file(LTSMinFolder,LibFolder,'prob2lts-sym',Opts),
192 move_file(LTSMinFolder,LibFolder,'prob2lts-dist',Opts),
193 move_file(LTSMinFolder,LibFolder,'ltsmin-printtrace',Opts),
194 my_system_call('rm',['-rf',LTSMinFolder],Opts).
195 complete_installation(z3,LibFolder,LocalLibFile,zip(FilesToExtract),Opts) :- !,
196 unzip_files(LibFolder,LocalLibFile,FilesToExtract,Opts),
197 format_with_colour_nl(user_output,[blue],'Make sure that the library in ~w can be found.',[LibFolder]),
198 ld_library_path(LDPATH),
199 format_with_colour_nl(user_output,[blue],'You need to set the environment variable ~w, e.g., as follows:',[LDPATH]),
200 format_with_colour_nl(user_output,[blue],' ~w=~w:$~w probcli -repl',[LDPATH,LibFolder,LDPATH]).
201 complete_installation(cvc5,LibFolder,LocalLibFile,zip(FilesToExtract),Opts) :- !,
202 % the cvc5 extension finds the libraries in the lib folder via its rpath, no environment variable is needed
203 unzip_files(LibFolder,LocalLibFile,FilesToExtract,Opts).
204 complete_installation(_,_,_,_,_). % nothing to do
205
206 % extract a single file or a list of files from a zip archive into LibFolder and delete the archive
207 unzip_files(LibFolder,ZipFile,FilesToExtract,Opts) :-
208 (FilesToExtract = [_|_] -> Files = FilesToExtract ; Files = [FilesToExtract]),
209 append(['-j', '-o', '-d', LibFolder, ZipFile],Files,Args), % -j: junk paths, -o: overwrite existing files
210 my_system_call('unzip',Args,Opts),
211 my_system_call('rm',['-rf',ZipFile],Opts).
212
213 ld_library_path(Path) :- host_platform(P), ld_library_path(P,Path).
214 ld_library_path(linux,'LD_LIBRARY_PATH').
215 ld_library_path(darwin,'DYLD_LIBRARY_PATH').
216 ld_library_path(windows,'PATH').
217
218 move_file(From,To,File,Opts) :-
219 ajoin([From,'/',File],FF), %path join
220 my_system_call('mv',[FF,To],Opts).
221
222 my_system_call(Cmd,Options,Opts) :-
223 ajoin_with_sep(Options,' ',OL),
224 (member(dryrun,Opts)
225 -> format('~w ~w~n',[Cmd,OL])
226 ; absolute_file_name(path(Cmd),
227 FullCmd,
228 [access(exist),extensions(['.exe','']),solutions(all),file_errors(fail)])
229 ->
230 format_with_colour_nl(user_output,[blue],' --> ~w ~w',[FullCmd,OL]),
231 system_call(FullCmd,Options,_OutputText,ErrText,Exit),
232 (Exit=exit(0) -> true
233 ; format_with_colour_nl(user_error,[red],'~w command failed (~w) : ~s',[Cmd,Exit,ErrText]),
234 fail
235 )
236 ; add_error(pathes_lib,'Cannot execute command:',Cmd),
237 format_with_colour_nl(user_error,[blue],'Try executing the command by hand:~n ~w ~w~n',[Cmd,OL]),
238 fail
239 ).
240
241 % --------------------
242
243 safe_load_foreign_resource(SourceModule,Lib) :-
244 % print(loading_foreign_resource(Lib)),nl,flush_output,
245 catch(safe_load_foreign_resource2(SourceModule,Lib), E, (
246 host_processor(Proc),
247 (host_platform(darwin) -> host_processor(Proc),
248 ajoin(['Could not load library ',Lib,
249 ', be sure to set LD_LIBRARY_PATH to include the lib folder of ProB for the right architecture (',
250 Proc,'). Exception:'],Msg)
251 ; host_platform(linux) ->
252 ajoin(['Could not load library ',Lib,
253 ', be sure to set LD_LIBRARY_PATH to include the lib folder of ProB on Linux. Exception:'],Msg)
254 ; ajoin(['Could not load library ',Lib, '. Exception:'],Msg)
255 ),
256 safe_add_error(Lib,Msg,E),
257 fail
258 )).
259
260 % check for existence error
261 % we need to prefix load_foreign_resource with the right module
262 safe_load_foreign_resource2(SourceModule,Lib) :-
263 E=error(existence_error(_,_),_),
264 debug_format(9,'Loading foreign resource module ~w from ~w~n',[SourceModule,Lib]),
265 flush_output, % flush output in case of crash (e.g., Killed: 9 on macOS)
266 catch(SourceModule:load_foreign_resource(library(Lib)), E, (
267 prob_lib_folder(LibF),
268 ajoin(['Could not load library ',Lib,
269 ', check that it is available in the lib folder ',LibF,
270 ' of ProB (you can run probcli -check_lib). Exception:'],Msg),
271 safe_add_error(Lib,Msg,E),
272 check_lib_component_available(Lib),
273 fail
274 )).
275
276 safe_add_error(Lib,Msg,E) :-
277 E2=error(existence_error(_,_),_),
278 catch(error_manager:add_error(Lib,Msg,E), E2, % maybe because counter library could not be loaded
279 format_with_colour_nl(user_error,[red],'~w ~w~n',[Msg,E])).