Skip to main content

Browse the archive

https://github.com/EasyCrypt/easycrypt
05 April 2024, 19:20:55 UTC
Revision 92900c9f4290d631543ddf717e369c3cfd96cc22 authored by Pierre-Yves Strub on 09 December 2015, 16:46:57 UTC, committed by Pierre-Yves Strub on 09 December 2015, 16:49:49 UTC 
Crude detection of identity rewriting.
 
The mechanism is to forbid non-keyed matching in
`rewrite` when LHS && RHS of the rewriting equation
are convertible. Currently, the whole `rewrite` is rejected
if the matching succeeds but the result would result in a
identity rewriting. A better mechanism should embed
the identity detection rewriting mechanism into the form
matching one.
1 parent b3f11a9
Raw File
Tip revision: 92900c9f4290d631543ddf717e369c3cfd96cc22 authored by Pierre-Yves Strub on 09 December 2015, 16:46:57 UTC
Crude detection of identity rewriting.
Tip revision: 92900c9
Vagrantfile 
Vagrant.configure(2) do |config|

  project_name = File.dirname(__FILE__).split("/").last

  config.vm.provider "virtualbox" do |vb|
    vb.memory = 6144 # set VM memory to 6GB
  end
  config.vm.synced_folder ".", "/home/vagrant/#{project_name}"

  config.vm.define :ubuntu do |ubuntu_config|
    ubuntu_config.vm.box = "ubuntu/wily64"
  end

  config.vm.provision "shell", binary: true, privileged: false, inline: <<-SHELL
    echo "Installing dependencies from Ubuntu packages."
    sudo DEBIAN_FRONTEND=noninteractive apt-get install -qq -yy m4 opam libgmp-dev libpcre3-dev pkg-config emacs24
    echo "Initializing opam."
    opam init -q -a --compiler=4.02.1
    eval `opam config env`
    opam repository add easycrypt git://github.com/EasyCrypt/opam.git
    opam update
#    echo "Installing EasyCrypt and dependencies from OPAM packages."
#    opam install -q easycrypt ec-provers ec-proofgeneral
#    why3 config --detect -C /home/vagrant/.why3.conf
#    echo "(when (fboundp 'electric-indent-mode) (electric-indent-mode -1))
#(setq proof-output-tooltips nil) (load-file \\"~/.opam/4.02.1/share/ec-proofgeneral/generic/proof-site.el\\")" >> /home/vagrant/.emacs
    echo "Installing EasyCrypt dependencies from OPAM packages."
    opam install -q -y ec-toolchain.20150923 ec-provers
    why3 config --detect -C /home/vagrant/.why3.conf
    cd #{project_name}
    echo "Building EasyCrypt."
    make && make -C proofgeneral local
    echo "Now use vagrant ssh -- -X and make pg"
  SHELL

end
back to top