1 % (c) 2022-2025 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_path_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(pathes, [runtime_application_path/1]).
24 :- use_module(pathes_extensions_db, [compile_time_unavailable_extension/2,
25 prob_extension/1, lib_component_implements_extension/4, lib_file_suffix/3]).
26 :- use_module(tools_platform, [host_platform/1, host_processor/1]).
27 :- use_module(tools_printing,[format_with_colour_nl/4]).
28 :- use_module(error_manager).
29 :- use_module(preferences, [get_preference/2]).
30 :- use_module(probsrc(tools_strings),[ajoin/2, ajoin_with_sep/3]).
31 :- use_module(system_call).
32 :- use_module(debug,[debug_format/3]).
33
34 % The predicates in this module can only be called at runtime,
35 % because they check whether certain files are present in the lib directory.
36 % For compile-time checks,
37 % use compile_time_unavailable_extension/2 from the pathes_extensions_db module instead
38 % (possibly with an additional runtime check).
39
40 add_file_suffix(Name,Kind,FullFile) :-
41 host_platform(Platform),
42 lib_file_suffix(Kind,Platform,Suffix),
43 atom_concat(Name,Suffix,FullFile).
44
45 lib_component_full_path(executable,Name,ltsmin_extension,FullFile) :-
46 !,
47 get_preference(path_to_ltsmin,LTSMinRel),
48 runtime_application_path(ProBHome),
49 absolute_file_name(LTSMinRel,LTSMinAbs,[relative_to(ProBHome)]),
50 add_file_suffix(Name,executable,File),
51 absolute_file_name(File,FullFile,[relative_to(LTSMinAbs)]).
52 lib_component_full_path(Kind,Name,_,FullFile) :-
53 add_file_suffix(Name,Kind,File),
54 absolute_file_name(prob_lib(File),FullFile).
55
56 check_lib_component_available(Component) :-
57 lib_component_available(Component,_Kind,_Name,FullFile,_ProBExtension,Available),
58 (Available=true
59 -> add_message(Component,'File for component is available: ',FullFile)
60 ; add_warning(Component,'File for component does not exist: ',FullFile)
61 ).
62
63 lib_component_available(C,Kind,Name,FullFile,ProBExtension,Available) :-
64 ? lib_component_implements_extension(C,Kind,Name,ProBExtension),
65 lib_component_full_path(Kind,Name,ProBExtension,FullFile),
66 (file_exists(FullFile) -> Available=true ; Available=false).
67
68 unavailable_extension(E, Reason) :- compile_time_unavailable_extension(E, Reason), !.
69 unavailable_extension(E, Reason) :-
70 ? lib_component_available(_Component, _Kind, _Name, FullFile, E, false),
71 atom_concat('required file missing: ', FullFile, Reason).
72
73 available_extension(E) :-
74 prob_extension(E),
75 \+ unavailable_extension(E,_).
76
77 prob_lib_folder(F) :- absolute_file_name(prob_lib('/'),F).
78
79 check_lib_contents(Stream,Verbose) :-
80 check_lib_contents(Stream,_,Verbose).
81 check_lib_contents(Stream,Comp,Verbose) :-
82 prob_lib_folder(FF),
83 (Verbose=silent -> true ; format_with_colour_nl(Stream,[blue],'Checking contents of lib folder: ~w',[FF])),
84 lib_component_available(Comp,Kind,_Name,_FullFile,ProBExtension,Available),
85 (Available=true
86 -> (Verbose=verbose -> format_with_colour_nl(Stream,[green],'~w (~w) found',[Comp,Kind])
87 ; true
88 )
89 ; format_with_colour_nl(Stream,[red],'~w (~w) not found, ~w not available',[Comp,Kind,ProBExtension]),
90 format_with_colour_nl(Stream,[blue],' * to install component run: probcli --install ~w~n',[Comp])
91 ),
92 fail.
93 check_lib_contents(_,_,_).
94
95 ltsmin_url('https://github.com/utwente-fmt/ltsmin/releases').
96
97 url(ltsmin,linux,_,
98 'https://github.com/utwente-fmt/ltsmin/releases/download/v3.0.2/','ltsmin-v3.0.2-linux.tgz',tgz).
99 url(ltsmin,darwin,_, % these are Intel binaries; but they run under Rosetta
100 'https://github.com/utwente-fmt/ltsmin/releases/download/v3.0.2/','ltsmin-v3.0.2-osx.tgz',tgz).
101
102 url(ltl2ba,linux,x86_64,'https://stups.hhu-hosting.de/downloads/ltl2ba_pl/sicstus4.8/linux-x86_64/','ltl2ba.so',bundle).
103 url(ltl2ba,darwin,_,'https://stups.hhu-hosting.de/downloads/ltl2ba_pl/sicstus4.8/macos/','ltl2ba.bundle',bundle).
104 url(ltl2ba,windows,x86_64,'https://stups.hhu-hosting.de/downloads/ltl2ba_pl/sicstus4.8/windows-x86_64/','ltl2ba.dll',bundle).
105 url(setlog,_,_,'https://stups.hhu-hosting.de/downloads/setlog_wrapper/','setlog-cli.qlf',qlf).
106
107
108 url7(Component,Plat,Proc,URL,File,Localfile,Kind) :- Localfile=File,
109 url(Component,Plat,Proc,URL,File,Kind).
110 url7(plantuml,_,_,'https://github.com/plantuml/plantuml/releases/download/v1.2024.8/','plantuml-epl-1.2024.8.jar','plantuml.jar',jar).
111
112 % 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
113
114 install_lib_component(Component,Opts) :-
115 host_platform(Plat),
116 host_processor(Proc),
117 url7(Component,Plat,Proc,URL,File,Localfile,_Kind),!,
118 install_lib_component_aux(Component,URL,File,Localfile,Opts).
119 install_lib_component(Component,_) :-
120 host_platform(Plat),
121 host_processor(Proc),
122 url(Component,Plat,RProc,_,_,_), % we know the component and there are rules
123 Proc \= RProc,!, % but not for this processor
124 add_error(install_lib_component,'No rules to install for this processor:',Component).
125 install_lib_component(Component,_) :-
126 host_platform(Plat),
127 url(Component,RPlat,_,_,_,_), % we know the component and there are rules
128 Plat \= RPlat,!, % but not for this platform
129 add_error(install_lib_component,'No rules to install on this platform:',Component).
130 install_lib_component(Component,_) :-
131 add_error(install_lib_component,'Unknown component, no rules to install:',Component).
132
133
134 install_lib_component_aux(Component,URL,File,Localfile,Opts) :-
135 (member(silent,Opts) -> true
136 ; format_with_colour_nl(user_output,[blue],'Installing component ~w from ~w',[Component,URL])),
137 ajoin([URL,File],FullURL),
138 absolute_file_name(prob_lib(Localfile),LocalLibFile),
139 my_system_call('curl',['-L',FullURL,'-o',LocalLibFile],Opts), % will not work on Windows
140 % TODO: we could use curl -I FullURL to detect if file exists; we should get HTTP/1.1 200 OK
141 prob_lib_folder(LibFolder),
142 complete_installation(Component,LibFolder,LocalLibFile,Opts),
143 !,
144 (member(dryrun,Opts) -> true ; format_with_colour_nl(user_output,green,'Installation complete',[])).
145 install_lib_component_aux(Component,_,_,_,_) :-
146 add_error(install_lib_component,'Installation of component failed:',Component).
147
148 % perform steps after downloading file
149 complete_installation(ltsmin,LibFolder,LocalLibFile,Opts) :- !,
150 my_system_call('tar',['-xvzf',LocalLibFile,'-C',LibFolder],Opts), % creates v3.0.2 folder
151 ajoin([LibFolder,'/v3.0.2/bin'],LTSMinFolder),
152 move_file(LTSMinFolder,LibFolder,'prob2lts-seq',Opts),
153 move_file(LTSMinFolder,LibFolder,'prob2lts-sym',Opts),
154 move_file(LTSMinFolder,LibFolder,'prob2lts-dist',Opts),
155 move_file(LTSMinFolder,LibFolder,'ltsmin-printtrace',Opts),
156 my_system_call('rm',['-rf',LTSMinFolder],Opts).
157 complete_installation(_,_,_,_). % nothing to do
158
159
160 move_file(From,To,File,Opts) :-
161 ajoin([From,'/',File],FF), %path join
162 my_system_call('mv',[FF,To],Opts).
163
164 my_system_call(Cmd,Options,Opts) :-
165 ajoin_with_sep(Options,' ',OL),
166 (member(dryrun,Opts)
167 -> format('~w ~w~n',[Cmd,OL])
168 ; absolute_file_name(path(Cmd),
169 FullCmd,
170 [access(exist),extensions(['.exe','']),solutions(all),file_errors(fail)])
171 ->
172 format_with_colour_nl(user_output,[blue],' --> ~w ~w',[FullCmd,OL]),
173 system_call(FullCmd,Options,_OutputText,ErrText,Exit),
174 (Exit=exit(0) -> true
175 ; format_with_colour_nl(user_error,[red],'~w command failed (~w) : ~s',[Cmd,Exit,ErrText]),
176 fail
177 )
178 ; add_error(pathes_lib,'Cannot execute command:',Cmd),
179 format_with_colour_nl(user_error,[blue],'Try executing the command by hand:~n ~w ~w~n',[Cmd,OL]),
180 fail
181 ).
182
183 % --------------------
184
185 safe_load_foreign_resource(SourceModule,Lib) :-
186 % print(loading_foreign_resource(Lib)),nl,flush_output,
187 catch(safe_load_foreign_resource2(SourceModule,Lib), E, (
188 host_processor(Proc),
189 (host_platform(darwin) -> host_processor(Proc),
190 ajoin(['Could not load library ',Lib,
191 ', be sure to set LD_LIBRARY_PATH to include the lib folder of ProB for the right architecture (',
192 Proc,'). Exception:'],Msg)
193 ; host_platform(linux) ->
194 ajoin(['Could not load library ',Lib,
195 ', be sure to set LD_LIBRARY_PATH to include the lib folder of ProB on Linux. Exception:'],Msg)
196 ; ajoin(['Could not load library ',Lib, '. Exception:'],Msg)
197 ),
198 safe_add_error(Lib,Msg,E),
199 fail
200 )).
201
202 % check for existence error
203 % we need to prefix load_foreign_resource with the right module
204 safe_load_foreign_resource2(SourceModule,Lib) :-
205 E=error(existence_error(_,_),_),
206 debug_format(9,'Loading foreign resource module ~w from ~w~n',[SourceModule,Lib]),
207 flush_output, % flush output in case of crash (e.g., Killed: 9 on macOS)
208 catch(SourceModule:load_foreign_resource(library(Lib)), E, (
209 ajoin(['Could not load library ',Lib,
210 ', check that it is available in the lib folder of ProB (you can run probcli -check_lib). Exception:'],Msg),
211 safe_add_error(Lib,Msg,E),
212 fail
213 )).
214
215 safe_add_error(Lib,Msg,E) :-
216 E2=error(existence_error(_,_),_),
217 catch(error_manager:add_error(Lib,Msg,E), E2, % maybe because counter library could not be loaded
218 format_with_colour_nl(user_error,[red],'~w ~w~n',[Msg,E])).