trywhy3: updated instructions

parent 0f574496
To compile and run TryWhy3 you need:
Instructions to build TryWhy3
-----------------------------
* 'ace'
* in subdirectory src/trywhy3/ do
in directory src/trywhy3 do
** install 'ace'
git clone https://github.com/ajaxorg/ace-builds.git
git clone https://github.com/ajaxorg/ace-builds.git
* Alt-Ergo
** install Alt-Ergo
** get sources of Alt-Ergo and put them in directory src/trywhy3
- get sources of Alt-Ergo and put them in directory src/trywhy3/ e.g. in
** change the following line of Makefile.in the name of this directory
src/trywhy3/alt-ergo-1.00-private-2015-01-29/
ALTERGODIR=src/trywhy3/alt-ergo-1.00-private-2015-01-29
- apply the patch alt-ergo.patch
** apply the patch alt-ergo.patch
cd <alt-ergo dir>
patch -p1 < ../alt-ergo.patch
cd <alt-ergo dir>
patch -p2 < ../alt-ergo.patch
- compile Alt-Ergo
./configure
make byte
* in the main directory
** if necessary, change the following line of Makefile.in to point
to Alt-Ergo sources
ALTERGODIR=src/trywhy3/alt-ergo-1.00-private-2015-01-29
** compile with
make trywhy3
* compile with make trywhy3
* install : TODO
diff -c -r alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.ml /home/cmarche/why3/src/trywhy3/alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.ml
*** alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.ml 2015-10-19 10:44:47.532877782 +0200
--- /home/cmarche/why3/src/trywhy3/alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.ml 2015-10-11 17:04:29.987623110 +0200
Only in alt-ergo-1.00-private-2015-01-29/: autom4te.cache
Only in alt-ergo-1.00-private-2015-01-29/: config.status
Only in alt-ergo-1.00-private-2015-01-29/: .depend
Only in alt-ergo-1.00-private-2015-01-29/: Makefile.configurable
diff -c -r /tmp/alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.ml alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.ml
*** /tmp/alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.ml 2016-04-07 16:01:57.449020746 +0200
--- alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.ml 2016-04-08 10:26:05.485174395 +0200
***************
*** 23,28 ****
--- 23,30 ----
......@@ -26,9 +30,9 @@ diff -c -r alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.ml /home/cmarche
end;
{ env with tbox = tbox; unit_tbox = utbox; inst = inst }
diff -c -r alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.mli /home/cmarche/why3/src/trywhy3/alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.mli
*** alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.mli 2015-10-19 10:44:47.540877782 +0200
--- /home/cmarche/why3/src/trywhy3/alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.mli 2015-10-11 17:05:07.655624228 +0200
diff -c -r /tmp/alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.mli alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.mli
*** /tmp/alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.mli 2016-04-07 16:01:57.449020746 +0200
--- alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.mli 2016-04-08 10:26:05.485174395 +0200
***************
*** 20,25 ****
--- 20,27 ----
......@@ -40,3 +44,28 @@ diff -c -r alt-ergo-1.00-private-2015-01-29/src/sat/sat_solvers.mli /home/cmarch
module type S = sig
type t
diff -c -r /tmp/alt-ergo-1.00-private-2015-01-29/src/util/numbers.ml alt-ergo-1.00-private-2015-01-29/src/util/numbers.ml
*** /tmp/alt-ergo-1.00-private-2015-01-29/src/util/numbers.ml 2016-04-07 16:01:57.453020790 +0200
--- alt-ergo-1.00-private-2015-01-29/src/util/numbers.ml 2016-04-08 10:41:51.037337014 +0200
***************
*** 20,28 ****
(* This file is distributed under the terms of the CeCILL-C licence *)
(******************************************************************************)
! module MyZarith = ZarithNumbers
module MyNums = NumsNumbers
! include MyZarith
--- 20,29 ----
(* This file is distributed under the terms of the CeCILL-C licence *)
(******************************************************************************)
! (* module MyZarith = ZarithNumbers *)
module MyNums = NumsNumbers
! include MyNums
!
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment