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