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])).