Here are some resources to help you get started with Deduce.
To get started with Deduce, follow these steps:
You can find the releases of Deduce on github. The most recent patches can be obtained by directly downloading the source code.
You will need Python version 3.10 or later. Here are some instructions and links to the download for various systems.
You will also need to install the Lark parsing library, which you can do by running the following command in the same directory as deduce.py
python -m pip install larkYou can write Deduce in any text editor you want, and run it through the terminal.
For the following editors, we have developed extensions that improve the experience of writing Deduce code.
Deduce is run by providing the deduce.py script with a *.pf file.
Suppose you have the following program. (defined in a file hello.pf)
This program defines a new union type called Greeting,
defines a variable world, and prints it out.
To run it, type the following command, or use the run functionality provided by your deduce editor.
python deduce.py hello.pfYou should see the output
hello
hello.pf is validThis introduction to Deduce has two parts. The first part gives a tutorial on how to write programs in Deduce. The second part shows how to write proofs in Deduce.
I recommend that you work through the examples in this introduction. Create a file named examples.pf in the top deduce directory and add the examples one at a time. To check the file, run the deduce.py script on the file from the deduce directory.
The Deduce Reference manual is linked below. It provides an alphabetical list of all the features in Deduce. The Cheat Sheet gives some advice regarding proof strategy and which Deduce keyword to use next in a proof. The Syntax Overview page provides a brief overview of the syntax structure of deduce.
The deduce.py script supports command line arguments which are
documented below. If an argument is not preceded by one of the
keywords listed below, then it is treated as the name of a file or
directory and will be processed by Deduce.
--dir directory-name
Tells Deduce to include the given directory-name in the list of
directories to search when importing a file. For example, if test.pf
imports Curry, and Curry.pf resides in a folder named howard,
then --dir howard will allow test.pf to import Church. Note that
--dir expects a directory name, not an individual file.
The rest of the command line arguments are useful primarily for the authors of Deduce. Users of Deduce can ignore them.
--no-stdlib
Deduce, by default, will include the directory of the standard library
(in /lib of the Deduce repository) in the list of directories to
search when importing a file. However if this argument is supplied, it
will not do so.
--lalr
Deduce normally uses a custom recursive descent parser to parse any
input files, however this argument will make Deduce instead use lark's
LALR parser. This argument exists solely for checking that
Deduce.lark maintains parity with the recursive descent parser.
--recursive-descent
Tells Deduce to use the recursive descent (default) parser. If
--lalr is also supplied, then only the recursive descent parser will
be used.
--recursive-directories or -r
Instead of only processing files in the specified directories, Deduce will also descend into any subdirectories.
--suppress-theorems
When a file contains one or more proof declarations inside of it, Deduce will create a .thm file. However, this argument makes it such that Deduce never creates such files.
--traceback
Prints out the exception if processing a file triggers an error.
--unique-names
Prints out all variables and types with an unique name. For example,
if a program defines a variable x in several different scopes, x
would instead be printed out as x.1 in one scope and printed as
x.2 in a different scope.
--verbose
Makes Deduce print out the debug logs. It is generally recommended to
use --traceback instead, as this argument can make Deduce print out
thousands of lines.
--error
Deduce will expect all files that it processes to contain an error. If there is a file that does not contain an error, Deduce will exit with a return code of 255.