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