pathes_lib

add_file_suffix(Name,Kind,FullFile) :-
    host_platform(Platform),
    lib_file_suffix(Kind,Platform,Suffix),
    atom_concat(Name,Suffix,FullFile).

available_extension(E) :-
    prob_extension(E),
    \+ unavailable_extension(E,_).

check_lib_contents(Stream,Verbose) :-
    check_lib_contents(Stream,_,Verbose).

check_lib_contents(Stream,Comp,Verbose) :-
    prob_lib_folder(FF),
    (Verbose=silent -> true ; format_with_colour_nl(Stream,[blue],'Checking contents of lib folder: ~w',[FF])),
    lib_component_available(Comp,Kind,_Name,_FullFile,ProBExtension,Available),
    (Available=true
    -> (Verbose=verbose -> format_with_colour_nl(Stream,[green],'~w (~w) found',[Comp,Kind])
    ; true
    )
    ; format_with_colour_nl(Stream,[red],'~w (~w) not found, ~w not available',[Comp,Kind,ProBExtension]),
    format_with_colour_nl(Stream,[blue],' * to install component run: probcli --install ~w~n',[Comp])
    ),
    fail.

check_lib_contents(_,_,_).

complete_installation(ltsmin,LibFolder,LocalLibFile,Opts) :- !,
    my_system_call('tar',['-xvzf',LocalLibFile,'-C',LibFolder],Opts), % creates v3.0.2 folder
    ajoin([LibFolder,'/v3.0.2/bin'],LTSMinFolder),
    move_file(LTSMinFolder,LibFolder,'prob2lts-seq',Opts),
    move_file(LTSMinFolder,LibFolder,'prob2lts-sym',Opts),
    move_file(LTSMinFolder,LibFolder,'prob2lts-dist',Opts),
    move_file(LTSMinFolder,LibFolder,'ltsmin-printtrace',Opts),
    my_system_call('rm',['-rf',LTSMinFolder],Opts).

complete_installation(_,_,_,_). % nothing to do

install_lib_component(Component,Opts) :-
    host_platform(Plat),
    host_processor(Proc),
    url7(Component,Plat,Proc,URL,File,Localfile,_Kind),!,
    install_lib_component_aux(Component,URL,File,Localfile,Opts).

install_lib_component(Component,_) :-
    host_platform(Plat),
    host_processor(Proc),
    url(Component,Plat,RProc,_,_,_), % we know the component and there are rules
    Proc \= RProc,!, % but not for this processor
    add_error(install_lib_component,'No rules to install for this processor:',Component).

install_lib_component(Component,_) :-
    host_platform(Plat),
    url(Component,RPlat,_,_,_,_), % we know the component and there are rules
    Plat \= RPlat,!, % but not for this platform
    add_error(install_lib_component,'No rules to install on this platform:',Component).

install_lib_component(Component,_) :-
    add_error(install_lib_component,'Unknown component, no rules to install:',Component).

install_lib_component_aux(Component,URL,File,Localfile,Opts) :-
    (member(silent,Opts) -> true
    ; format_with_colour_nl(user_output,[blue],'Installing component ~w from ~w',[Component,URL])),
    ajoin([URL,File],FullURL),
    absolute_file_name(prob_lib(Localfile),LocalLibFile),
    my_system_call('curl',['-L',FullURL,'-o',LocalLibFile],Opts), % will not work on Windows
    % TODO: we could use curl -I FullURL to detect if file exists; we should get HTTP/1.1 200 OK
    prob_lib_folder(LibFolder),
    complete_installation(Component,LibFolder,LocalLibFile,Opts),
    !,
    (member(dryrun,Opts) -> true ; format_with_colour_nl(user_output,green,'Installation complete',[])).

install_lib_component_aux(Component,_,_,_,_) :-
    add_error(install_lib_component,'Installation of component failed:',Component).

lib_component_available(C,Kind,Name,FullFile,ProBExtension,Available) :-
    lib_component_implements_extension(C,Kind,Name,ProBExtension),
    lib_component_full_path(Kind,Name,ProBExtension,FullFile),
    (file_exists(FullFile) -> Available=true ; Available=false).

lib_component_full_path(executable,Name,ltsmin_extension,FullFile) :-
    !,
    get_preference(path_to_ltsmin,LTSMinRel),
    runtime_application_path(ProBHome),
    absolute_file_name(LTSMinRel,LTSMinAbs,[relative_to(ProBHome)]),
    add_file_suffix(Name,executable,File),
    absolute_file_name(File,FullFile,[relative_to(LTSMinAbs)]).

lib_component_full_path(Kind,Name,_,FullFile) :-
    add_file_suffix(Name,Kind,File),
    absolute_file_name(prob_lib(File),FullFile).

ltsmin_url('https://github.com/utwente-fmt/ltsmin/releases').

move_file(From,To,File,Opts) :-
    ajoin([From,'/',File],FF), %path join
    my_system_call('mv',[FF,To],Opts).

my_system_call(Cmd,Options,Opts) :-
    ajoin_with_sep(Options,' ',OL),
    (member(dryrun,Opts)
    -> format('~w ~w~n',[Cmd,OL])
    ; absolute_file_name(path(Cmd),
    FullCmd,
    [access(exist),extensions(['.exe','']),solutions(all),file_errors(fail)])
    ->
    format_with_colour_nl(user_output,[blue],' --> ~w ~w',[FullCmd,OL]),
    system_call(FullCmd,Options,_OutputText,ErrText,Exit),
    (Exit=exit(0) -> true
    ; format_with_colour_nl(user_error,[red],'~w command failed (~w) : ~s',[Cmd,Exit,ErrText]),
    fail
    )
    ; add_error(pathes_lib,'Cannot execute command:',Cmd),
    format_with_colour_nl(user_error,[blue],'Try executing the command by hand:~n ~w ~w~n',[Cmd,OL]),
    fail
).

prob_lib_folder(F) :- absolute_file_name(prob_lib('/'),F).

safe_add_error(Lib,Msg,E) :-
    E2=error(existence_error(_,_),_),
    catch(error_manager:add_error(Lib,Msg,E), E2, % maybe because counter library could not be loaded
    format_with_colour_nl(user_error,[red],'~w ~w~n',[Msg,E])).

safe_load_foreign_resource(SourceModule,Lib) :-
    % print(loading_foreign_resource(Lib)),nl,
    catch(safe_load_foreign_resource2(SourceModule,Lib), E, (
    host_processor(Proc),
    (host_platform(darwin) -> host_processor(Proc),
    ajoin(['Could not load library ',Lib,
    ', be sure to set LD_LIBRARY_PATH to include the lib folder of ProB for the right architecture (',
    Proc,'). Exception:'],Msg)
    ; host_platform(linux) ->
    ajoin(['Could not load library ',Lib,
    ', be sure to set LD_LIBRARY_PATH to include the lib folder of ProB on Linux. Exception:'],Msg)
    ; ajoin(['Could not load library ',Lib, '. Exception:'],Msg)
    ),
    safe_add_error(Lib,Msg,E),
    fail
)).

safe_load_foreign_resource2(SourceModule,Lib) :-
    E=error(existence_error(_,_),_),
    catch(SourceModule:load_foreign_resource(library(Lib)), E, (
    ajoin(['Could not load library ',Lib,
    ', check that it is available in the lib folder of ProB (you can run probcli -check_lib). Exception:'],Msg),
    safe_add_error(Lib,Msg,E),
    fail
)).

unavailable_extension(E, Reason) :- compile_time_unavailable_extension(E, Reason), !.

unavailable_extension(E, Reason) :-
    lib_component_available(_Component, _Kind, _Name, FullFile, E, false),
    atom_concat('required file missing: ', FullFile, Reason).

url(ltsmin,linux,_,
    'https://github.com/utwente-fmt/ltsmin/releases/download/v3.0.2/','ltsmin-v3.0.2-linux.tgz',tgz).

url(ltsmin,darwin,_, % these are Intel binaries; but they run under Rosetta
    'https://github.com/utwente-fmt/ltsmin/releases/download/v3.0.2/','ltsmin-v3.0.2-osx.tgz',tgz).

url(ltl2ba,linux,x86_64,'https://stups.hhu-hosting.de/downloads/ltl2ba_pl/sicstus4.8/linux-x86_64/','ltl2ba.so',bundle).

url(ltl2ba,darwin,_,'https://stups.hhu-hosting.de/downloads/ltl2ba_pl/sicstus4.8/macos/','ltl2ba.bundle',bundle).

url(ltl2ba,windows,x86_64,'https://stups.hhu-hosting.de/downloads/ltl2ba_pl/sicstus4.8/windows-x86_64/','ltl2ba.dll',bundle).

url(setlog,_,_,'https://stups.hhu-hosting.de/downloads/setlog_wrapper/','setlog-cli.qlf',qlf).

url7(Component,Plat,Proc,URL,File,Localfile,Kind) :- Localfile=File,
    url(Component,Plat,Proc,URL,File,Kind).

url7(plantuml,_,_,'https://github.com/plantuml/plantuml/releases/download/v1.2024.7/','plantuml-epl-1.2024.7.jar','plantuml.jar',jar).