Pour utiliser cette machine virtuelle, vous devez installer VirtualBox et Vagrant.
Pour l'interface graphique (utilisée par Why3), il vous faudra un serveur X11 :
- sous MacOS, utilisez XQuartz, soit avec
brew install --cask xquartz, soit à partir de https://www.xquartz.org/ - sous Windows, utilisez VcXsrv
Dans un répertoire de votre choix (il sera utilisé par la suite pour y mettre les fichiers utilisés avec cette machine virtuelle, dans le répertoire /home/vagrant/workspace), placez ce fichier Vagrantfile, puis :
sous Windows PowerShell :
- lancez le serveur X11 avec :
$env:Path += ";C:\Program Files\VcXsrv"$env:DISPLAY = "localhost:0"vcxsrv :0 -multiwindow
- construisez la machine virtuelle avec :
vagrant up(peut prendre du temps la première fois à cause du téléchargement de la VM)
- connectez-vous à la machine virtuelle avec :
vagrant ssh
sous MacOS :
- lancez le serveur X11 avec :
open -a XQuartz
- autorisez les connexions locales avec :
xhost +localhost
- construisez la machine virtuelle avec :
vagrant up(peut prendre du temps la première fois à cause du téléchargement de la VM)
- connectez-vous à la machine virtuelle avec :
vagrant ssh
sous Linux, les commandes vagrant devraient suffire.
Test
Pour tester votre machine, vous pouvez copier ce fichier dans le répertoire, puis dans la machine virtuelle, exécuter : cd workspace; why3 ide prog.mlw. L'utilisation de Tools > Provers > Alt-Ergo devrait suffire à prouver les obligations de preuve de ce programme.
Vous pouvez également faire le petit exemple Soufflé décrit sur https://souffle-lang.github.io/simple
Arrêt
Quand vous avez terminé, quittez le shell de la machine virtuelle avec Ctrl-D ou exit. Vous pouvez vous connecter de nouveau à la machine virtuelle avec vagrant ssh. Si vous ne comptez pas utiliser la machine virtuelle pendant un moment, vous pouvez l'arrêter avec vagrant halt. Vous devrez la démarrer de nouveau avec vagrant up avant de pouvoir vous y connecter, mais cela sera rapide car l'image est déjà téléchargée.
Vous pouvez également contrôler cette machine virtuelle à partir de l'application Virtual Box.