tcsprojects / mlsolver

A tool for solving the satisfiability and validity problems for modal fixpoint logics.
9 stars 1 forks source link

installation err #1

Closed astefano closed 7 years ago

astefano commented 7 years ago

Hi,

I get this with make:

ocamlbuild main.native + /usr/bin/ocamlc -c -I pgsolver/src/pgsolver -I pgsolver/tests -I pgsolver/temp -I pgsolver/satsolversforocaml/src -I pgsolver/satsolversforocaml/src/preprocessor -I pgsolver/satsolversforocaml/src/minisat -I pgsolver/satsolversforocaml/src/pseudosat -I pgsolver/satsolversforocaml/src/zchaff -I pgsolver/satsolversforocaml/src/externalsat -I pgsolver/satsolversforocaml/src/picosat -I pgsolver/src/generators -I pgsolver/src/tools -I pgsolver/src/paritygame -I pgsolver/src/solvers -I pgsolver/src/generators/modelchecking -I pgsolver/src/generators/policyiter -I pgsolver/src/generators/policyiter/generators -I pgsolver/src/solvers/stratimpralgs -I pgsolver/tcslib/src/utils -I pgsolver/tcslib/src/formula -I pgsolver/tcslib/src/data -I pgsolver/tcslib/src/automata -I pgsolver/tcslib/src/formula/pdl -I pgsolver/tcslib/src/formula/parser -I pgsolver/tcslib/src/formula/ltmc -I pgsolver/tcslib/src/formula/ltl -I pgsolver/tcslib/src/formula/ctlstar -I pgsolver/tcslib/src/formula/mmc -I pgsolver/tcslib/src/formula/lmmc -I pgsolver/tcslib/src/automata/parser -I src/generators -I src/pgsolvers -I src/tools -I src/automata -I src/mlsolver -I src/automata/pdl -I src/automata/ltmc -I src/automata/ctlstar -I src/automata/ctl -I src/automata/mmc -I src/automata/lmmc -o pgsolver/src/pgsolver/main.cmo pgsolver/src/pgsolver/main.ml File "pgsolver/src/pgsolver/main.ml", line 9, characters 5-17: Error: Unbound module Generatedsat Command exited with code 2. Compilation unsuccessful after building 124 targets (0 cached) in 00:00:04. Makefile:8: recipe for target 'solver' failed make: *** [solver] Error 10

Any clue how i could fix this?

Cheers, Lacramioara

oliverfriedmann commented 7 years ago

Hi there,

Was that a clean install or did you "upgrade" a pre-existing installation? I just tried setting up MLSolver from scratch: git clone https://github.com/tcsprojects/mlsolver.git Cloning into 'mlsolver'... remote: Counting objects: 192, done. remote: Compressing objects: 100% (12/12), done. remote: Total 192 (delta 0), reused 0 (delta 0), pack-reused 180 Receiving objects: 100% (192/192), 106.37 KiB | 0 bytes/s, done. Resolving deltas: 100% (76/76), done. Olivers-MacBook-Pro:tmp oliverfriedmann$ cd mlsolver Olivers-MacBook-Pro:mlsolver oliverfriedmann$ git submodule update --init Submodule 'pgsolver' (https://github.com/oliverfriedmann/pgsolver.git) registered for path 'pgsolver' Cloning into '/Users/oliverfriedmann/Temp/tmp/mlsolver/pgsolver'... Submodule path 'pgsolver': checked out 'e11df0bdbe9423c69afeeee9449c0decef17909d' Olivers-MacBook-Pro:mlsolver oliverfriedmann$ cd pgsolver Olivers-MacBook-Pro:pgsolver oliverfriedmann$ git submodule update --init Submodule 'satsolversforocaml' (https://github.com/oliverfriedmann/satsolversforocaml) registered for path 'satsolversforocaml' Submodule 'scripts/policyitervis/metapostgraphs' (https://github.com/oliverfriedmann/metapostgraphs.git) registered for path 'scripts/policyitervis/metapostgraphs' Submodule 'tcslib' (https://github.com/oliverfriedmann/tcslib.git) registered for path 'tcslib' Cloning into '/Users/oliverfriedmann/Temp/tmp/mlsolver/pgsolver/satsolversforocaml'... Cloning into '/Users/oliverfriedmann/Temp/tmp/mlsolver/pgsolver/scripts/policyitervis/metapostgraphs'... Cloning into '/Users/oliverfriedmann/Temp/tmp/mlsolver/pgsolver/tcslib'... Submodule path 'satsolversforocaml': checked out 'cfd1d6b296fc12f68fd31a6bf94b1b7267a7649b' Submodule path 'scripts/policyitervis/metapostgraphs': checked out '8e8e42b6a4ece0a877c7c6e93217109d39ad5753' Submodule path 'tcslib': checked out 'd5f1af9c03c8874d943da97a27c68a257882e416' Olivers-MacBook-Pro:pgsolver oliverfriedmann$ cd .. Olivers-MacBook-Pro:mlsolver oliverfriedmann$ make ocamlbuild main.native Finished, 240 targets (0 cached) in 00:00:11. mv main.native bin/mlsolver ocamlbuild pdlsudoku.native Finished, 4 targets (0 cached) in 00:00:00. mv pdlsudoku.native bin/pdlsudokugenerator ocamlbuild ctlstarsudoku.native Finished, 4 targets (0 cached) in 00:00:00. mv ctlstarsudoku.native bin/ctlstarsudokugenerator ocamlbuild mucalcsudoku.native Finished, 4 targets (0 cached) in 00:00:00. mv mucalcsudoku.native bin/mucalcsudokugenerator ocamlbuild ltmcparitybuechi.native Finished, 4 targets (0 cached) in 00:00:00. mv ltmcparitybuechi.native bin/ltmcparitybuechigenerator ocamlbuild elevatorts.native Finished, 4 targets (0 cached) in 00:00:00. mv elevatorts.native bin/elevatortsgenerator ocamlbuild philosophersts.native Finished, 4 targets (0 cached) in 00:00:00. mv philosophersts.native bin/philosopherstsgenerator ocamlbuild guarded_trafo_worst_case.native Finished, 36 targets (32 cached) in 00:00:00. mv guarded_trafo_worst_case.native bin/guarded_trafo_worst_case

astefano commented 7 years ago

clean install...

i've just tried now to install pgsolver (like at https://github.com/tcsprojects/pgsolver) and i can run it:

lacra@lacra-VirtualBox:~/tools/pgsolver$ bin/pgsolver testcases/failtest1.gm PGSolver Collection Ver. 4.0: Parity Game Solver Authors: Oliver Friedmann (University of Munich) and Martin Lange (University of Kassel), 2008-2016 http://tcsprojects.org Parsing ............................... 0.25 sec Chosen not to solve at all. Player 0 wins from nodes: {} with strategy [] Player 1 wins from nodes: {} with strategy []

so i tried to run make inside mlsolver/pgsolver first and then do make in mlsolver, but i get another err: lacra@lacra-VirtualBox:~/tools/mlsolver$ make solver ocamlbuild main.native + /home/lacra/.opam/4.03.0/bin/ocamlopt.opt pgsolver/satsolversforocaml/src/satwrapper.cmx pgsolver/satsolversforocaml/src/satsolvers.cmx pgsolver/src/pgsolver/basics.cmx pgsolver/tcslib/src/data/tcsbasedata.cmx pgsolver/tcslib/src/data/tcsarray.cmx pgsolver/tcslib/src/data/tcslist.cmx pgsolver/tcslib/src/data/tcsset.cmx pgsolver/tcslib/src/data/tcscache.cmx pgsolver/tcslib/src/data/tcsgraph.cmx pgsolver/src/paritygame/paritygame.cmx pgsolver/src/paritygame/generators.cmx pgsolver/src/pgsolver/info.cmx pgsolver/src/generators/cliquegame.cmx pgsolver/tcslib/src/data/tcsmaths.cmx pgsolver/src/generators/clusteredrandomgame.cmx pgsolver/src/generators/jurdzinskigame.cmx pgsolver/src/generators/laddergame.cmx pgsolver/src/generators/langincl.cmx pgsolver/src/generators/modelcheckerladder.cmx pgsolver/src/generators/modelchecking/mucalculus.cmx pgsolver/src/generators/modelchecking/elevators.cmx pgsolver/src/generators/randomgame.cmx pgsolver/src/generators/recursiveladder.cmx pgsolver/src/generators/steadygame.cmx pgsolver/src/generators/towersofhanoi.cmx pgsolver/src/paritygame/generatorlist.cmx pgsolver/tcslib/src/automata/parser/tcsgameparserinternal.cmx pgsolver/tcslib/src/automata/parser/tcsparitygameparser.cmx pgsolver/tcslib/src/automata/parser/tcsparitygamelexer.cmx pgsolver/tcslib/src/automata/parser/tcsparitysolutionparser.cmx pgsolver/tcslib/src/automata/parser/tcsparitysolutionlexer.cmx pgsolver/tcslib/src/utils/tcstiming.cmx pgsolver/tcslib/src/automata/tcsgames.cmx pgsolver/tcslib/src/automata/parser/tcsgameparser.cmx pgsolver/src/paritygame/parsers.cmx pgsolver/src/paritygame/solvers.cmx pgsolver/tcslib/src/data/tcsqueue.cmx pgsolver/src/paritygame/specialsolve.cmx pgsolver/src/paritygame/transformations.cmx pgsolver/tcslib/src/data/tcsstrings.cmx pgsolver/src/paritygame/univsolve.cmx pgsolver/src/solvers/recursive.cmx pgsolver/src/solvers/smallprogress.cmx pgsolver/src/solvers/bigstep.cmx pgsolver/src/solvers/dominiondecomp.cmx pgsolver/src/solvers/fpiter.cmx pgsolver/tcslib/src/utils/tcsargs.cmx pgsolver/src/solvers/genetic.cmx pgsolver/src/solvers/guessstrategy.cmx pgsolver/src/solvers/localmodelchecker.cmx pgsolver/src/solvers/optstratimprov.cmx pgsolver/src/solvers/satsolve.cmx pgsolver/src/solvers/stratimpralgs.cmx pgsolver/src/solvers/stratimpralgs/switch_cunningham.cmx pgsolver/src/solvers/stratimpralgs/switch_globally_best.cmx pgsolver/src/solvers/stratimpralgs/switch_history.cmx pgsolver/src/solvers/stratimpralgs/switch_internal.cmx pgsolver/src/solvers/stratimpralgs/switch_locally_best.cmx pgsolver/src/solvers/stratimpralgs/switch_random.cmx pgsolver/src/solvers/stratimpralgs/switch_snare.cmx pgsolver/src/solvers/stratimpralgs/switch_zadeh.cmx pgsolver/src/solvers/stratimprdisc.cmx pgsolver/src/solvers/stratimprlocal.cmx pgsolver/src/solvers/stratimprlocal2.cmx pgsolver/src/solvers/stratimprovement.cmx pgsolver/src/solvers/stratimprsat.cmx pgsolver/src/solvers/viasat.cmx pgsolver/src/paritygame/solverlist.cmx pgsolver/src/paritygame/verification.cmx pgsolver/src/pgsolver/whoiswho.cmx pgsolver/temp/generatedsat.cmx pgsolver/src/pgsolver/main.cmx -o pgsolver/src/pgsolver/main.native File "_none_", line 1: Error: No implementations provided for the following modules: Big_int referenced from pgsolver/tcslib/src/data/tcsmaths.cmx Str referenced from pgsolver/src/generators/modelchecking/mucalculus.cmx Command exited with code 2. Compilation unsuccessful after building 276 targets (0 cached) in 00:00:14. Makefile:8: recipe for target 'solver' failed make: *** [solver] Error 10

oliverfriedmann commented 7 years ago

I can reproduce it now, will push a fix shortly.

astefano commented 7 years ago

Thanks a lot!

oliverfriedmann commented 7 years ago

Hi there,

Can you try again? Note that the installation instructions now contain one more line.

Cheers, Oliver

astefano commented 7 years ago

Great, thanks a bunch!