Revision 2998c271bc3a30c4c351c4d39943cf720390cad4 authored by Pierre-Yves Strub on 01 December 2015, 17:10:55 UTC, committed by Pierre-Yves Strub on 01 December 2015, 17:29:46 UTC
Add a new hint mechanism for auto-applying lemmas. Lemmas are added to the auto base with: `hint exact : L1 ... Ln.` `trivial` (and all relatives) now tries to close any goal it is presented by applying one of the lemmas of the database --- closing any generated subgoal recursively. The lemmas in the hint database are not used when `trivial` tries to close the subgoals. Lemmas are applied using a rigid unification and with the view mechanism disabled. The current implementation is linear in the size of the database. A pre-selection mechanism may be necessary in case the hint database grows too much.
1 parent 7cc81de
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
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...