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(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
96		% url(Component,Platform,Processor,URL,File,Kind)
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.9/linux-x86_64/','ltl2ba.so',bundle).
103		url(ltl2ba,darwin,_,'https://stups.hhu-hosting.de/downloads/ltl2ba_pl/sicstus4.9/macos/','ltl2ba.bundle',bundle).
104		url(ltl2ba,windows,x86_64,'https://stups.hhu-hosting.de/downloads/ltl2ba_pl/sicstus4.9/windows-x86_64/','ltl2ba.dll',bundle).
105		url(setlog,_,_,'https://stups.hhu-hosting.de/downloads/setlog_wrapper/','setlog-cli.qlf',qlf).
106		url(z3,darwin,aarch64,Z3,'z3-5.0.0-arm64-osx-13.3.zip',
107		zip('z3-5.0.0-arm64-osx-13.3/bin/libz3.dylib')) :- z3_url(Z3).
108		url(z3,darwin,x86_64,Z3,'z3-5.0.0-x64-osx-13.3.zip',
109		zip('z3-5.0.0-x64-osx-13.3/bin/libz3.dylib')) :- z3_url(Z3).
110		url(z3,darwin,x86_64,Z3,'z3-5.0.0-x64-win.zip',
111		zip('z3-5.0.0-x64-win/bin/libz3.dylib')) :- z3_url(Z3).
112		url(z3,linux,x86_64,Z3,'z3-5.0.0-x64-glibc-2.39.zip',
113		zip('z3-5.0.0-x64-glibc-2.39/bin/libz3.dylib')) :- z3_url(Z3).
114
115		z3_url('https://github.com/Z3Prover/z3/releases/download/z3-5.0.0/').
116		%ltsmin_url('https://github.com/utwente-fmt/ltsmin/releases').
117
118		url7(Component,Plat,Proc,URL,File,Localfile,Kind) :- Localfile=File,
119		url(Component,Plat,Proc,URL,File,Kind).
120		url7(plantuml,_,_,'https://github.com/plantuml/plantuml/releases/download/v1.2024.8/','plantuml-epl-1.2024.8.jar','plantuml.jar',jar).
121
122		% 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
123
124		install_lib_component(Component,Opts) :-
125		host_platform(Plat),
126		host_processor(Proc),
127		url7(Component,Plat,Proc,URL,File,Localfile,Kind),!,
128		install_lib_component_aux(Component,URL,File,Localfile,Kind,Opts).
129		install_lib_component(Component,_) :-
130		host_platform(Plat),
131		host_processor(Proc),
132		url(Component,Plat,RProc,_,_,_), % we know the component and there are rules
133		Proc \= RProc,!, % but not for this processor
134		add_error(install_lib_component,'No rules to install for this processor:',Component).
135		install_lib_component(Component,_) :-
136		host_platform(Plat),
137		url(Component,RPlat,_,_,_,_), % we know the component and there are rules
138		Plat \= RPlat,!, % but not for this platform
139		add_error(install_lib_component,'No rules to install on this platform:',Component).
140		install_lib_component(Component,_) :-
141		add_error(install_lib_component,'Unknown component, no rules to install:',Component).
142
143
144		install_lib_component_aux(Component,URL,File,Localfile,Kind,Opts) :-
145		(member(silent,Opts) -> true
146		; format_with_colour_nl(user_output,[blue],'Installing component ~w from ~w',[Component,URL])),
147		ajoin([URL,File],FullURL),
148		absolute_file_name(prob_lib(Localfile),LocalLibFile),
149		my_system_call('curl',['-L',FullURL,'-o',LocalLibFile],Opts), % will not work on Windows
150		% TODO: we could use curl -I FullURL to detect if file exists; we should get HTTP/1.1 200 OK
151		prob_lib_folder(LibFolder),
152		complete_installation(Component,LibFolder,LocalLibFile,Kind,Opts),
153		!,
154		(member(dryrun,Opts) -> true ; format_with_colour_nl(user_output,green,'Installation complete',[])).
155		install_lib_component_aux(Component,_,_,_,_,_) :-
156		add_error(install_lib_component,'Installation of component failed:',Component).
157
158		% perform steps after downloading file
159		complete_installation(ltsmin,LibFolder,LocalLibFile,_,Opts) :- !,
160		my_system_call('tar',['-xvzf',LocalLibFile,'-C',LibFolder],Opts), % creates v3.0.2 folder
161		ajoin([LibFolder,'/v3.0.2/bin'],LTSMinFolder),
162		move_file(LTSMinFolder,LibFolder,'prob2lts-seq',Opts),
163		move_file(LTSMinFolder,LibFolder,'prob2lts-sym',Opts),
164		move_file(LTSMinFolder,LibFolder,'prob2lts-dist',Opts),
165		move_file(LTSMinFolder,LibFolder,'ltsmin-printtrace',Opts),
166		my_system_call('rm',['-rf',LTSMinFolder],Opts).
167		complete_installation(z3,LibFolder,LocalLibFile,zip(FileToExtract),Opts) :- !,
168		my_system_call('unzip',['-j', '-o', '-d', LibFolder, % -j: junk paths, -o: overwrite existing libz3
169		LocalLibFile,FileToExtract],Opts),
170		my_system_call('rm',['-rf',LocalLibFile],Opts),
171		format_with_colour_nl(user_output,[blue],'Make sure that the library in ~w can be found.',[LibFolder]),
172		ld_library_path(LDPATH),
173		format_with_colour_nl(user_output,[blue],'You need to set the environment variable ~w, e.g., as follows:',[LDPATH]),
174		format_with_colour_nl(user_output,[blue],' ~w=~w:$~w probcli -repl',[LDPATH,LibFolder,LDPATH]).
175		complete_installation(_,_,_,_,_). % nothing to do
176
177		ld_library_path(Path) :- host_platform(P), ld_library_path(P,Path).
178		ld_library_path(linux,'LD_LIBRARY_PATH').
179		ld_library_path(darwin,'DYLD_LIBRARY_PATH').
180		ld_library_path(windows,'PATH').
181
182		move_file(From,To,File,Opts) :-
183		ajoin([From,'/',File],FF), %path join
184		my_system_call('mv',[FF,To],Opts).
185
186		my_system_call(Cmd,Options,Opts) :-
187		ajoin_with_sep(Options,' ',OL),
188		(member(dryrun,Opts)
189		-> format('~w ~w~n',[Cmd,OL])
190		; absolute_file_name(path(Cmd),
191		FullCmd,
192		[access(exist),extensions(['.exe','']),solutions(all),file_errors(fail)])
193		->
194		format_with_colour_nl(user_output,[blue],' --> ~w ~w',[FullCmd,OL]),
195		system_call(FullCmd,Options,_OutputText,ErrText,Exit),
196		(Exit=exit(0) -> true
197		; format_with_colour_nl(user_error,[red],'~w command failed (~w) : ~s',[Cmd,Exit,ErrText]),
198		fail
199		)
200		; add_error(pathes_lib,'Cannot execute command:',Cmd),
201		format_with_colour_nl(user_error,[blue],'Try executing the command by hand:~n ~w ~w~n',[Cmd,OL]),
202		fail
203		).
204
205		% --------------------
206
207		safe_load_foreign_resource(SourceModule,Lib) :-
208		% print(loading_foreign_resource(Lib)),nl,flush_output,
209		catch(safe_load_foreign_resource2(SourceModule,Lib), E, (
210		host_processor(Proc),
211		(host_platform(darwin) -> host_processor(Proc),
212		ajoin(['Could not load library ',Lib,
213		', be sure to set LD_LIBRARY_PATH to include the lib folder of ProB for the right architecture (',
214		Proc,'). Exception:'],Msg)
215		; host_platform(linux) ->
216		ajoin(['Could not load library ',Lib,
217		', be sure to set LD_LIBRARY_PATH to include the lib folder of ProB on Linux. Exception:'],Msg)
218		; ajoin(['Could not load library ',Lib, '. Exception:'],Msg)
219		),
220		safe_add_error(Lib,Msg,E),
221		fail
222		)).
223
224		% check for existence error
225		% we need to prefix load_foreign_resource with the right module
226		safe_load_foreign_resource2(SourceModule,Lib) :-
227		E=error(existence_error(_,_),_),
228		debug_format(9,'Loading foreign resource module ~w from ~w~n',[SourceModule,Lib]),
229		flush_output, % flush output in case of crash (e.g., Killed: 9 on macOS)
230		catch(SourceModule:load_foreign_resource(library(Lib)), E, (
231		prob_lib_folder(LibF),
232		ajoin(['Could not load library ',Lib,
233		', check that it is available in the lib folder ',LibF,
234		' of ProB (you can run probcli -check_lib). Exception:'],Msg),
235		safe_add_error(Lib,Msg,E),
236		check_lib_component_available(Lib),
237		fail
238		)).
239
240		safe_add_error(Lib,Msg,E) :-
241		E2=error(existence_error(_,_),_),
242		catch(error_manager:add_error(Lib,Msg,E), E2, % maybe because counter library could not be loaded
243		format_with_colour_nl(user_error,[red],'~w ~w~n',[Msg,E])).