(Created page with "== The REPL of ProB == ProB provides various consoles, also called REPL (Read-Eval-Print-Loop). A REPL (Read-Eval-Print-Loop) or console can be used to evaluate formulas with ProB or issue other commands. ProB provides various REPLs, depending on which version of ProB you use: * The REPL in probcli can be started with the command <tt>-repl</tt> * The REPL in ProB Tcl/Tk is the Eval Console. * ProB2-UI also provides a console view Below we describe th...") |
|||
| Line 4: | Line 4: | ||
A REPL (Read-Eval-Print-Loop) or console can be used to evaluate formulas with ProB or issue other commands. | A REPL (Read-Eval-Print-Loop) or console can be used to evaluate formulas with ProB or issue other commands. | ||
ProB provides various REPLs, depending on which version of ProB you use: | ProB provides various REPLs, depending on which version of ProB you use: | ||
* The REPL in probcli can be started with the command <tt>-repl</tt> | * The REPL in [[Using_the_Command-Line_Version_of_ProB|probcli]] can be started with the command <tt>-repl</tt> | ||
* The REPL in ProB Tcl/Tk is the [[Eval_Console|Eval Console]]. | * The REPL in ProB Tcl/Tk is the [[Eval_Console|Eval Console]]. | ||
* ProB2-UI also provides a console view | * ProB2-UI also provides a console view | ||
Below we describe the REPL of probcli, which is the most powerful. Some (but not all) of the commands are available in the other consoles as well. | Below we describe the REPL of [[Using_the_Command-Line_Version_of_ProB|probcli]], which is the most powerful. Some (but not all) of the commands are available in the other consoles as well. | ||
=== Starting the REPL === | |||
You can start the REPL simply by typing: | |||
<pre> | |||
probcli -repl | |||
</pre> | |||
If you wish you can instruct probcli to also load and initialise a B machine and set other preferences before starting the REPL: | |||
<pre> | |||
probcli MYFILE.mch -repl -p REPL_UNICODE TRUE -pref-group integer int32 | |||
</pre> | |||
Here we have loaded a B machine MYFILE.mch and set MININT/MAXINT for 32 bit systems. | |||
The preference <tt>-p REPL_UNICODE TRUE</tt> instructs the REPL to display the formula again using Unicode operators (warning: this can slow down certain terminal applications). | |||
We also recommend you use the <tt>rlwrap</tt> tool available under Unix and Linux to start probcli, so that you have a command history: | |||
<pre> | |||
rlwrap probcli -repl | |||
</pre> | |||
=== Using the REPL === | |||
Every character following the <tt>>>></tt> until the end of the line is typed by the user. The next line, starting with ⇝, shows the Unicode rendering of the ASCII expression or predicate typed by the user. | |||
probcli -repl -p REPL_UNICODE TRUE | |||
ProB Interactive Expression and Predicate Evaluator | |||
Type ":help" for more information. | |||
Examples: see [[Sudoku Solved in the ProB REPL]] or [[Proving_Theorems_in_the_ProB_REPL]]. | Examples: see [[Sudoku Solved in the ProB REPL]] or [[Proving_Theorems_in_the_ProB_REPL]]. | ||
ProB provides various consoles, also called REPL (Read-Eval-Print-Loop). A REPL (Read-Eval-Print-Loop) or console can be used to evaluate formulas with ProB or issue other commands. ProB provides various REPLs, depending on which version of ProB you use:
Below we describe the REPL of probcli, which is the most powerful. Some (but not all) of the commands are available in the other consoles as well.
You can start the REPL simply by typing:
probcli -repl
If you wish you can instruct probcli to also load and initialise a B machine and set other preferences before starting the REPL:
probcli MYFILE.mch -repl -p REPL_UNICODE TRUE -pref-group integer int32
Here we have loaded a B machine MYFILE.mch and set MININT/MAXINT for 32 bit systems. The preference -p REPL_UNICODE TRUE instructs the REPL to display the formula again using Unicode operators (warning: this can slow down certain terminal applications).
We also recommend you use the rlwrap tool available under Unix and Linux to start probcli, so that you have a command history:
rlwrap probcli -repl
Every character following the >>> until the end of the line is typed by the user. The next line, starting with ⇝, shows the Unicode rendering of the ASCII expression or predicate typed by the user.
probcli -repl -p REPL_UNICODE TRUE ProB Interactive Expression and Predicate Evaluator Type ":help" for more information.
Examples: see Sudoku Solved in the ProB REPL or Proving_Theorems_in_the_ProB_REPL.