[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] TLAPM from command line

From: Ioannis Filippidis <jfili...@xxxxxxxxx>
Date: Fri, 10 Mar 2017 13:41:02 -0800
Organization: California Institute of Technology
References: <b5de1b24-7fb2-4298-9e09-97d5fc67c8c2@googlegroups.com> <30bcf803-e43d-4ddc-953b-dcf1ce3b8f45@gmail.com>
User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.12; rv:45.0) Gecko/20100101 Thunderbird/45.7.1

Hi Amira,

`polyml` is available on GitHub [1], where past releases can be found tagged,
and on SourceForge [2]. I could build Isabelle 2011-1 using `polyml == 5.4.0`
but not the version suggested in Isabelle's README. Isabelle 2011-1 also needed
a few modifications to circumvent some errors discussed on its mailing list.

Please see the installation notes I've copied below for more details
(these notes may contain errors or missing steps).
These worked in 2016 on a Debian x86_64 GNU/Linux 9 (stretch).

(The latest `polyml` is available to install with the package manager on
Debian, but newer than what is needed for Isabelle 2011-1.)

[1] https://github.com/polyml/polyml
[2] https://sourceforge.net/projects/polyml/files/polyml

Best regards,
ioannis


---- BEGIN INSTALLATION NOTES ----

# install TLAPS from linux tar
mkdir $HOME/tlaps
cd tlaps
curl -LO https://tla.msr-inria.inria.fr/tlaps/dist/current/tlaps-1.4.3.tar.gz
tar -zxf *.tar.gz


# zenon
cd tlaps-1.4.3/zenon
./configure --prefix $HOME
make
make install
which zenon
zenon --help
cd ..


# Poly/ML (for Isabelle 2011-1)
# `polyml` in apt is too new for Isabelle 2011-1
# apt-get install polyml
# Isabelle 2011-1 requires >= 5.2.1 in its README,
# but that version raises errors
# download from:
https://sourceforge.net/projects/polyml/files/polyml/5.4.0
tar -zxf polyml.5.4.tar.gz
cd polyml.5.4
./configure --prefix=$HOME/tlaps/polyml/
make -j4
make install
which poly
poly --version
add $HOME/tlaps/polyml/bin to $PATH


# Isabelle 2011-1
# download from:
http://isabelle.in.tum.de/website-Isabelle2011-1/download.html
tar -xzf Isabelle2011-1.tar.gz
cd Isabelle2011-1
#
# copy comment.sty` under `lib/texinputs`
# from here: https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-January/msg00167.html
#
# in `etc/settings` set:
# ML_HOME="$HOME/tlaps/polyml/bin"
#
# comment the outer conditional in `lib/scripts/getsettings`:
# if [ -z "$ISABELLE_SETTINGS_PRESENT" ]
# then
# fi
# https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-February/msg00107.html
#
# add at the top of `lib/Tools/browser`
# source $HOME/tlaps/Isabelle2011-1/lib/scripts/getsettings
#
./build
# you can also `cd src/Pure; isabelle make` but docs won't build later
add $HOME/tlaps/Isabelle2011-1/bin/ to $PATH


# compile TLA+ formalization in Isabelle
cd isabelle
make
cd ..


# compile TLAPS
apt-get install ocaml ocaml-batteries-included ocaml-native-compilers
ocaml -version
cd tlapm
./configure --prefix $HOME
make all
make install
which tlapm
tlapm --config
cd examples/cantor
tlapm -C --verbose Cantor1.tla


# install more backends

## z3
apt-get install z3 spass


## ls4 (propositional temporal prover)
git clone git@xxxxxxxxxx:quickbeam123/ls4.git
cd ls4/core
make
cp ls4 $HOME/bin


## translator to input format of `ls4`
curl -LO http://cgi.csc.liv.ac.uk/~konev/software/trp++/translator/translate.tar.bz2
tar xvfj translate.tar.bz2
cd translate/
./build.sh
cp translate $HOME/bin/ptl_to_trp


## CVC3
# http://www.cs.nyu.edu/acsys/cvc3/doc/INSTALL.html
apt-get install bison flex libgmp-dev
curl -LO http://www.cs.nyu.edu/acsys/cvc3/releases/2.4.1/cvc3-2.4.1.tar.gz
tar -xzf cvc3*.tar.gz
cd cvc3*
./configure --prefix=$HOME/cvc3
make
cd test
make
bin/test
make install


# TLA+ tools
curl -LO https://tla.msr-inria.inria.fr/tlatoolbox/dist/tla.zip
unzip tla.zip -d $HOME/tlatools
cd github
git clone git@xxxxxxxxxx:joewilliams/tla_tools
mkdir /tmp/tla2tex
mkdir /tmp/tlc

==== END INSTALLATION NOTES ====


On 3/10/17 11:53 AM, 'Martin' via tlaplus wrote:
> Hi Amira,
>
> Yes, you can run tlapm on the commandline, by default it should be
> installed in /usr/local/lib/bin/tlapm . It seems you are trying to
> install from source, but there are also binary packages available at:
>
> http://tla.msr-inria.inria.fr/tlaps/content/Download/Binaries.html
>
> They also provide the binaries for Zenon, Isabelle 2011 and other
> theorem provers. If you would like to compile from source, I would
> advise to install the binary package first to have all the backends
> ready ( they are by default installed to /usr/local/lib/tlapm ) and then
> install your self-compiled copy of tlapm to /usr/local/bin . That should
> also solve your problems with PolyML, which is only necessary for
> compiling (and running) Isabelle.
>
> I hope that helps a bit,
> cheers Martin
>
> On 03/10/2017 03:52 PM, Amira Methni wrote:
>> Hi, 
>>
>> I have a set of TLA+ modules containing several lemma and proofs. I want
>> to write a script that launches TLAPs for all these modules instead of
>> launching TLAPS for each TLA+ file separately. 
>> Can I use TLAPM from command line to do this? 
>>
>> PS: I tried to install TLAPS source code by following instructions on
>> the web site, but polyml is no longer available.
>>
>> Thanks  
>> Amira
>>

Follow-Ups:
- Re: [tlaplus] TLAPM from command line
  - From: Amira Methni
- Re: [tlaplus] TLAPM from command line
  - From: Amira Methni

References:
- TLAPM from command line
  - From: Amira Methni
- Re: [tlaplus] TLAPM from command line
  - From: Martin

Prev by Date: Re: [tlaplus] TLAPM from command line
Next by Date: Re: Announcing Sbuilder - a tool to generate TLA+ model for business IT systems
Previous by thread: Re: [tlaplus] TLAPM from command line
Next by thread: Re: [tlaplus] TLAPM from command line
Index(es):
- Date
- Thread