-
Notifications
You must be signed in to change notification settings - Fork 9
Running SASyLF
SASyLF is a proof checker; it checks proofs written in its specialized proof language. It can be run on the command-line in the same way as (for example) a Java compiler. It can also be run by using the plugin with the Eclipse IDE.
If starting out new, the best way is to choose File > New > Project ... and then choose SASyLF Wizards > SASyLF Project. This will ask for a name and a "proof folder". For the proof folder, please use the default "slf" -- other choices will make it harder to use the IDE. Then once the project is created, select the proof folder and then use File > New > Other ... and in SASyLF Wizards you can create a Proof File. This will get you a file in which you can edit a SASyLF proof. The Wiki has several pages for the syntax to use.
Once you have a proof file in the editor, it is checked whenever you save it. But if you are doing a lot of proof writing, it is helpful to use the SASyLF perspective, which has a few other benefits. To use it, choose Window > Perspective > Open Perspective > Other... and choose the SASyLF perspective. This adds some tools, some menus and displays SASyLF proof packages in a similar way to Java packages in the Java Perspective.
The SASyLF menu has an "About" choice, but more importantly, two common commands: "Check Proofs" to check the proof without saving it and "Correct Indentation". Each has a short-hand: respectively, Meta zero or Meta I. Checking proofs can also be accomplished using the tool button in the form of a green check mark.
It is beneficial to have an "Outline View" open when editing a proof file. The outline shows all the top-level declarations in short-hand. Judgments and syntax declarations have a tree view to show their contents. The triangle can be clicked to open/close these parts. Clicking on a name will move the editor to that declaration.
Errors are show with a red mark in the margins of the editor, and (usually) with squiggly lines in the body of the editor. More information can be found by hovering over either mark. If the red mark in the left margin has a super-imposed light-bulb, it means that a "Quick Fix" is available. This can be found by clicking on the margin icon, or from Eclipse's errors views. Errors in a different section can be seen in the right margin ruler which covers the whole file.
There are two kinds of errors: fatal (parse) errors cause SASyLF to stop processing the file, and non-fatal errors. The former error will usually be the only error (but some non-fatal parse errors may have been signalled earlier). These should be fixed to enable SASyLF to build an internal representation so that other checks can be done. If most of your errors go away suddenly, it usually means not they they are fixed but that they are hidden by a fatal parse error.
Occasionally, SASyLF will indicate an "Internal Error". Please report these to the developers, including the proof file that was being checked.
When writing a proof, one often doesn't remember the precise name and arguments of a theorem. After writing "by theorem s" one can press control-space to get a list of theorems starting with "s". Typing more will reduce the list. And each possibility is associated with its header. Then once one writes "on", the system will remind you of the declaration of the parameter(s) needed. This system is especially useful when using a large builton module such as "Natural". Completion sometimes doesn't work if the outline view is damaged or not open.
You will need a Java distribution, preferably Java 8, but later versions are likely to work as well. You will also need a JAR file, either from SASyLF's release page or built yourself. The Eclipse plugin file works fine. Then you run the proof checker from the JAR as in
java -jarfilename.jaroptions path/to/filename.slfThe following options are supported:
-
--helpPrint out full list of options -
--versionPrint the version and exit -
--verbosePrint extra information while checking proofs -
--compwhereWarn if implicit bindings are not reflected inwhereclauses -
--path=... Specify a path for finding SASyLF proof files -
--LFprint extra information for errors, including internal forms and information useful for quick fixes.