Setting up Linux Machines using Suse manually for use of SPARK Ada and why3 via File Manager (Computer Science, Swansea University)
The following are the steps for configuring the settings in the Linux
Lab so that SPARK Ada and why3 can be started from the file Manager without
using the Command Shell.
- Please study the file
in Linux explaining the basic terminology of Linux
such as directory, ~/bin etc.
- Setting up scripts for calling SPARK Ada (gps) and why3
- Copy the following two files to your directory ~/bin
(by right clicking on the links and using "Safe link as "; remember
~/bin is the subdirectory bin of Home)
- Some Webbrowsers will safe the files as callgps.txt and callwhy3.txt.
Rename them using the file manager to callgps and callwhy3.
- Make them executable by
- navigating with the File Manager to ~/bin
- right clicking on each of the two files and choosing Properties
-> Permissions -> Advanced Permissions
- click for row "Owner" on the one item in column with header "x" so that you get a green tick.
- This tick means that the file is executable by Owner.
- Now we associate files with extension .gpr with "callgps" and
.mlw with "callwhy3"
For .gpr this is done as follows (for .mlw do the same replacing
gpr by mlw and callgps by callwhy3)
- From the start menu (bottom left) search for "File associations" and choose "File Associations"
- Press on the bottom of the menu "+ Add"
- Choose as Group "application", and as name gpr
- In the side menu under "application" you find an entry which is
initially at the bottom called "gpr" (it will later be sorted alphabetically).
- Left click on it.
- You want that on the right side you have as filename patterns
exactly one entry containing *.gpr
This can be obtained by pressing the "+ Add" button and then typing in
*.gpr and pressing return.
- Under Application Preference Order you want that there is
exaclty one entry callgps.
This is obtained by pressing the "+ Add" button.
Then choose the file icon. Navigate to ~/bin
- Choose "callgps"
- Press Apply
- Press okay
- Repeat the same with file extension *.mlw and application callwhy3
- Now close all File Managers (called Dolphin) since they won't have this
file association yet.
- Make sure that you don't use file names and paths containing blanks.
In Linux many scripts (as the ones I have written) don't work if you have blanks.
Replace blanks by underscore "_".
- If you now navigate using a new file manager to a directory containing
a SPARK Ada project, and left click on main.gpr gps is opened for this
- One more thing: for being able to run why3 we need to configure
- Note: As of 19 Oct 2017 the why3 system is not yet installed in the Linux Lab.
Installation of why3 is a bit more complicated and we will use the why3 system only later in the course.
You can ignore the following until the why3 system has been installed.
- Done by running from a command shell (terminal or console)
/usr/local/opam/system/bin/why3 config --detect-provers
- Output put would be somthing like
Found prover Z3 version 4.3.2, Ok.
Found prover CVC4 version 1.4, Ok.
Found prover CVC3 version 2.4.1, Ok.
Warning: prover Coq version 8.4pl5 is not known to be supported.
3 provers detected and 1 provers detected with unsupported version
Save config to /home/123485/.why3.conf
- Now try out why3 by
- navigating on the File Manager to
an SPARK Ada project containing pre- and post-condtion,
- navigate to the generted subdirectory gnatprove
- and clicking on a file with extension .mlw
- Now study basic usage instructions of SPARK Ada