From 727fbd9619c7deb22c7a30e30b77f86776aef234 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Wed, 3 Feb 2021 17:50:36 +0100
Subject: [PATCH] Remove Prolog section whose content can be found on the wiki
---
.../user/52_Prolog/00_section_header.adoc | 4 -
.../52_Prolog/Building_ProB_on_Windows.adoc | 72 ----
.../user/52_Prolog/Getting_Involved.adoc | 135 -------
.../Organization_of_ProB_Sources.adoc | 5 -
.../ProB's_Prolog_Datastructures.adoc | 177 ---------
.../52_Prolog/Prolog_Coding_Guidelines.adoc | 130 -------
.../52_Prolog/Running_ProB_from_source.adoc | 66 ----
.../chapter/user/52_Prolog/Why_Prolog.adoc | 364 ------------------
.../user/52_Prolog/ZZ_section_footer.adoc | 2 -
9 files changed, 955 deletions(-)
delete mode 100644 src/docs/chapter/user/52_Prolog/00_section_header.adoc
delete mode 100644 src/docs/chapter/user/52_Prolog/Building_ProB_on_Windows.adoc
delete mode 100644 src/docs/chapter/user/52_Prolog/Getting_Involved.adoc
delete mode 100644 src/docs/chapter/user/52_Prolog/Organization_of_ProB_Sources.adoc
delete mode 100644 src/docs/chapter/user/52_Prolog/ProB's_Prolog_Datastructures.adoc
delete mode 100644 src/docs/chapter/user/52_Prolog/Prolog_Coding_Guidelines.adoc
delete mode 100644 src/docs/chapter/user/52_Prolog/Running_ProB_from_source.adoc
delete mode 100644 src/docs/chapter/user/52_Prolog/Why_Prolog.adoc
delete mode 100644 src/docs/chapter/user/52_Prolog/ZZ_section_footer.adoc
diff --git a/src/docs/chapter/user/52_Prolog/00_section_header.adoc b/src/docs/chapter/user/52_Prolog/00_section_header.adoc
deleted file mode 100644
index c51697c..0000000
--- a/src/docs/chapter/user/52_Prolog/00_section_header.adoc
+++ /dev/null
@@ -1,4 +0,0 @@
-
-[[prob-prolog-guide]]
-= ProB Prolog Guide
-:leveloffset: +1
diff --git a/src/docs/chapter/user/52_Prolog/Building_ProB_on_Windows.adoc b/src/docs/chapter/user/52_Prolog/Building_ProB_on_Windows.adoc
deleted file mode 100644
index e263a07..0000000
--- a/src/docs/chapter/user/52_Prolog/Building_ProB_on_Windows.adoc
+++ /dev/null
@@ -1,72 +0,0 @@
-
-[[building-prob-on-windows]]
-= Building ProB on Windows
-
-In case that you want to compile ProB from Source on Windows (XP),
-here are some information about the setup:
-
-== Required
-
-1. Sicstus (4.1.3)
-2. Visual Studio 2005
-3. TCL 8.5 (Activestate)
-4. Cygwin & svn
-5. ant
-6. jsch jar file copied into the c:\ant\lib folder
-
-To start the build process run ant from within the buildscript folder of
-ProB. Here is the output of the env command on a working installation.
-
-Most important are PATH, LIB and INCLUDE. Note that this was a german
-version of Windows XP.
-
-----
-HOMEPATH=\Dokumente und Einstellungen\hudson
-MANPATH=/usr/local/man:/usr/share/man:/usr/man:
-APPDATA=C:\Dokumente und Einstellungen\hudson\Anwendungsdaten
-HOSTNAME=TERRA
-TERM=cygwin
-PROCESSOR_IDENTIFIER=x86 Family 6 Model 30 Stepping 5, GenuineIntel
-WINDIR=C:\WINDOWS
-VS80COMNTOOLS=C:\Programme\Microsoft Visual Studio 8\Common7\Tools\
-OLDPWD=/usr/bin
-USERDOMAIN=TERRA
-OS=Windows_NT
-ALLUSERSPROFILE=C:\Dokumente und Einstellungen\All Users
-ANT_HOME=c:\ant
-USER=hudson
-COMMONPROGRAMFILES=C:\Programme\Gemeinsame Dateien
-LIB=C:\Programme\Microsoft Visual Studio 8\VC\lib;C:\Programme\Microsoft Visual Studio 8\SDK\v2.0\Lib;C:\Programme\Microsoft Visual Studio 8\VC\PlatformSDK\Lib
-USERNAME=hudson
-PROCESSOR_LEVEL=6
-PATH=/usr/local/bin:/usr/bin:/bin:/cygdrive/c/Tcl/bin:/cygdrive/c/WINDOWS/system32:/cygdrive/c/WINDOWS:/cygdrive/c/WINDOWS/System32/Wbem:/cygdrive/c/ant/bin:"C:/Programme/SICStus Prolog 4.1.3/bin":/cygdrive/c/Programme/Microsoft Visual Studio 8/SDK/v2.0/Bin:/cygdrive/c/WINDOWS/Microsoft.NET/Framework/v2.0.50727:/cygdrive/c/Programme/Microsoft Visual Studio 8/VC/bin:/cygdrive/c/Programme/Microsoft Visual Studio 8/Common7/IDE:/cygdrive/c/Programme/Microsoft Visual Studio 8/VC/vcpackages
-FP_NO_HOST_CHECK=NO
-PWD=/home/hudson
-SYSTEMDRIVE=C:
-JAVA_HOME=C:\Programme\Java\jdk1.6.0_23
-LANG=C.UTF-8
-USERPROFILE=C:\Dokumente und Einstellungen\hudson
-CLIENTNAME=Console
-PS1=\[\e]0;\w\a\]\n\[\e[32m\]\u@\h \[\e[33m\]\w\[\e[0m\]\n\$
-LOGONSERVER=\\TERRA
-PROCESSOR_ARCHITECTURE=x86
-!C:=C:\cygwin\bin
-SHLVL=1
-HOME=/home/hudson
-PATHEXT=.COM;.EXE;.BAT;.CMD;.VBS;.VBE;.JS;.JSE;.WSF;.WSH;.tcl
-HOMEDRIVE=C:
-PROMPT=$P$G
-COMSPEC=C:\WINDOWS\system32\cmd.exe
-SYSTEMROOT=C:\WINDOWS
-PRINTER=
-CVS_RSH=/bin/ssh
-PROCESSOR_REVISION=1e05
-CL=/FIC:\cygwin\home\hudson\prob\VC8_redist_x86\targetsxs.h
-INFOPATH=/usr/local/info:/usr/share/info:/usr/info:
-PROGRAMFILES=C:\Programme
-NUMBER_OF_PROCESSORS=4
-INCLUDE=C:\Programme\Microsoft Visual Studio 8\VC\include;C:\Programme\Microsoft Visual Studio 8\SDK\v2.0\include
-SESSIONNAME=Console
-COMPUTERNAME=TERRA
-_=/usr/bin/env
-----
diff --git a/src/docs/chapter/user/52_Prolog/Getting_Involved.adoc b/src/docs/chapter/user/52_Prolog/Getting_Involved.adoc
deleted file mode 100644
index 74d943b..0000000
--- a/src/docs/chapter/user/52_Prolog/Getting_Involved.adoc
+++ /dev/null
@@ -1,135 +0,0 @@
-
-[[getting-involved]]
-= Getting Involved
-
-[[the-prob-java-core-and-ui]]
-== The ProB Java Core and UI
-
-See the README in our https://github.com/bendisposto/prob[Github Repository]
-
-[[the-prolog-sources]]
-== The Prolog Sources
-
-If you want to contribute to the Prolog part of ProB, if you want to
-extend the ProB API, or need them as reference, you need the Prolog
-sources which can be downloaded from
-https://www3.hhu.de/stups/downloads/prob/source/[our source prob directory].
-To compile the sources you need a
-https://www.sics.se/projects/sicstus-prolog-leading-prolog-technology[SICStus Prolog]
-licence.
-
-[[running-prob-from-prolog]]
-== Running ProB from Prolog
-
-You first need to download and install
-https://www.sics.se/projects/sicstus-prolog-leading-prolog-technology[SICStus Prolog].
-Evaluation licenses (30-days) are available. You need SICStus 4.2 or
-newer (we will switch to SICStus 4.3 in summer or autumn of 2014).
-
-You need the password to download SICStus then run
-`sudo ./InstallSICStus` and provide the site name, license code and
-expiration date. Be sure to add the SICStus binaries to your PATH.
-
-Probably you should also install a recent Active Tcl distribution.
-
-Now, you need the ProB Prolog sources. If you have access to our Gitlab
-server then the information is here:
-https://www3.hhu.de/stups/downloads/prob/source/[Prolog Sources].
-
-Now, add the following to your `.bash_login` file (at least on Mac OS;
-supposing you cloned the Git repository into ~/git_root):
-
-....
-export PROBDIR=~/git_root/prob_prolog
-export PROB_SOURCE_DIR=$PROBDIR/src
-alias prob='cd $PROB_SOURCE_DIR; sicstus -Dprob_profile=true -l $PROB_SOURCE_DIR/prob_tcltk.pl --goal "go."'
-....
-
-Now, you can simply start ProB from the command-line and from source
-with `prob`.
-
-To start the Unit Test REPL, add the following to your `.bash_login`
-file (at least on Mac OS):
-
-`alias test='cd $PROBDIR; rlwrap sicstus -Dprob_safe_mode=true -l $PROB_SOURCE_DIR/test_runner.pl --goal "test_repl."`
-
-(It is recommended to install rlwrap so that you get a history of your
-commands. If you don't want to install rlwrap just remove it from the
-line above.)
-
-Before using ProB for the first time from source you should build the
-extensions. The minimal extensions are counter and user_signal. You can
-build them using
-
-....
-cd extensions/counter
-make
-cd ../user_signal
-make
-....
-
-You could also build all extensions at once by going to the top of the
-prob_prolog tree (i.e., the directory containing src and lib as
-sub-directories) and then type
-
-`make`
-
-On Mac you may have to add a symbolic link to gawk in order to build the
-ProZ fuzz extension:
-
-`sudo ln -s /usr/bin/awk /usr/bin/gawk`
-
-Now you can start the testing console using `test`. You can e.g. type
-the number of a unit test to run it, or a test category such as
-`tickets` to run all tests in that category.
-
-[[running-the-prolog-tests]]
-== Running the Prolog Tests
-
-All Prolog tests are stored as facts in the file `testcases.pl`. Every
-test has
-
-* an identifier (a number); the last test added has the highest number
-* a non-empty list of categories (such as unit, tickets,...)
-* the test itself: the parameters to `probcli` needed to run the test
-* a textual description of the test
-
-There is a specific `test_runner.pl` file for running all Prolog unit
-and integration tests. The test_runner also provides a REPL
-(read-eval-print-loop) for running tests and collection of tests.
-
-Supposing you have set the variable `PROBDIR` (see above) and have the
-`rlwrap` tool, you can define the following alias (e.g., in your
-`.bash_login` file on Mac OS X):
-
-`alias test='cd $PROBDIR; rlwrap sicstus -Dprob_safe_mode=true -l $PROBDIR/src/test_runner.pl --goal "test_repl."'`
-
-Now you can start the test runner:
-
-....
-$ test
-...
-SICStus 4.2.3 (x86_64-darwin-11.4.2): Fri Oct 5 15:58:35 CEST 2012
-Licensed to SP4phil-fak.uni-duesseldorf.de
-TEST ==> last.
-...
-All tests successful.
-Walltime: 100 ms
-....
-
-Some useful commands are:
-
-* last to run the last test added to `testcases.pl`
-* all to run all tests
-* cat to list all categories of tests (e.g., cbc, cbc_deadlock,...)
-* cbc, cbc_deadlock, tickets, ... : to run all tests in that category
-* type in a number to run the specific test with that number (see
-`testcases.pl`)
-* type in a range m-n to run all tests in that range
-* v or vv to switch to verbose or very verbose mode
-* q to quit the test runner (and stay in Prolog)
-* x to quit the test runner and Prolog
-* debug to switch on Prolog debug mode
-* trace to force Prolog to start tracing as soon as an error occurs (if
-you have switched to debug above then you will be able to inspect the
-Prolog goal stack)
diff --git a/src/docs/chapter/user/52_Prolog/Organization_of_ProB_Sources.adoc b/src/docs/chapter/user/52_Prolog/Organization_of_ProB_Sources.adoc
deleted file mode 100644
index c38d374..0000000
--- a/src/docs/chapter/user/52_Prolog/Organization_of_ProB_Sources.adoc
+++ /dev/null
@@ -1,5 +0,0 @@
-
-[[organization-of-prob-sources]]
-= Organization of ProB Sources
-
-The ProB sources consist of ...
diff --git a/src/docs/chapter/user/52_Prolog/ProB's_Prolog_Datastructures.adoc b/src/docs/chapter/user/52_Prolog/ProB's_Prolog_Datastructures.adoc
deleted file mode 100644
index db58607..0000000
--- a/src/docs/chapter/user/52_Prolog/ProB's_Prolog_Datastructures.adoc
+++ /dev/null
@@ -1,177 +0,0 @@
-
-[[probs-prolog-datastructures]]
-= ProB's Prolog Datastructures
-
-[[data-values]]
-== Data Values
-
-Integer value:
-
-`int(Nr)`
-
-where Nr is an integer
-
-Booleans:
-
-`pred_true` +
-`pred_false`
-
-Enumerated or deferred set elements:
-
-`fd(Nr,Type)`
-
-where Nr is an integer >= 1 and Type is an atom representing the type of
-enumerated/deferred set
-
-Strings
-
-`string(S)`
-
-where S is an atom
-
-Pairs/couples
-
-`(Val1,Val2)`
-
-where Val1 and Val2 are values
-
-Records
-
-`rec(Fields)`
-
-where Fields is a list of terms:
-
-`field(Name,Val)`
-
-where Name is atom representing the field name and Val is a value.
-
-The fields are sorted by name!
-
-Sets Here is an overview of the set representations:
-
-`[]` +
-`[Val|Set]` +
-`avl_set(AVL)` +
-`closure(P,T,B)` +
-`global_set(GS)` +
-`freetype(T)`
-
-The empty set is encoded as the empty list.
-
-`[]`
-
-This represents a set containing at least the value Val and the rest:
-
-`[Val|Set]`
-
-Note that Set can in principle be any other form (e.g., avl_set(.)). The
-predicate `expand_custom_set_to_list` can be used to transform a set
-into a form using only the empty list and the `[.|.]` functor.
-
-The next are called custom explicit sets, they always represent a fully
-known set.
-
-A set can be represented by a non-empty AVL tree:
-
-`avl_set(AVL)`
-
-Given a list of parameter identifiers, a list of types and a predicate
-AST B, we can represent the set \{P| P:T & B} as follows:
-
-`closure(P,T,B)`
-
-There are custom representations for complete types, these may be phased
-out in the future and replaced by the closure(.,.,.) representation:
-
-`global_set(GS)` +
-`freetype(T)`
-
-Freetype values
-
-`freeval(Id,Case,Value)`
-
-[[ast-abstract-syntax-tree]]
-== AST (Abstract Syntax Tree)
-
-An AST node has the form:
-
-`b(Expr,Type,Infos)`
-
-Expr generally has the form Functor(AST1,...,ASTk). Below we list
-possible cases. The predicate `syntaxelement` in bsyntaxtree.pl lists
-all allowed forms of Expr. Type is either `pred` for predicates, `subst`
-for substitutions or the value type for expressions, see below. Infos
-contains information about the AST node and is explained next.
-
-[[information-list]]
-=== Information list
-
-Infos should be a ground list of informations. Some important
-information fields are:
-
-`contains_wd_condition` +
-`used_ids(Ids)` +
-`nodeid(PositionInfo)` +
-`refers_to_old_state(References)`
-
-[[ast-types]]
-=== AST types
-
-Possible types are:
-
-`pred` +
-`subst` +
-`integer` +
-`boolean` +
-`string` +
-`global(G)` +
-`couple(Type1,Type2)` +
-`record(FieldTypes)` +
-`set(Type)` +
-`seq(Type)` +
-`freetype(F)`
-
-where FieldTypes is a list containing:
-
-`field(Name,Type)`
-
-[[operators-without-arguments]]
-=== Operators without arguments
-
-`boolean_false` +
-`boolean_true` +
-`bool_set`
-
-...
-
-[[unary-operators]]
-=== Unary operators
-
-`card(AST)` +
-`domain(AST)` +
-`front(AST)`
-
-...
-
-[[binary-operators]]
-=== Binary operators
-
-`cartesian_product(AST1,AST2)` +
-`composition(AST1,AST2)` +
-`concat(AST1,AST2)` +
-`conjunct(AST1,AST2)`
-
-...
-
-[[special-operators]]
-=== Special operators
-
-`general_sum(Ids,AST,AST)` +
-`general_product(Ids,AST,AST)` +
-`lambda(Ids,AST,AST)` +
-`quantified_union(Ids,AST,AST)` +
-`quantified_intersection(Ids,AST,AST)` +
-`set_extension(ListOfASTs)` +
-`sequence_extension(ListOfASTs)`
-
-...
diff --git a/src/docs/chapter/user/52_Prolog/Prolog_Coding_Guidelines.adoc b/src/docs/chapter/user/52_Prolog/Prolog_Coding_Guidelines.adoc
deleted file mode 100644
index e88baad..0000000
--- a/src/docs/chapter/user/52_Prolog/Prolog_Coding_Guidelines.adoc
+++ /dev/null
@@ -1,130 +0,0 @@
-
-[[prolog-coding-guidelines]]
-= Prolog Coding Guidelines
-
-[[general-guidelines]]
-General Guidelines
-------------------
-
-Please ensure that there are no compilation errors or warnings when
-checking in. Also, try to ensure that there are no errors when loading
-the files in Spider (Eclipse). Ideally, try to get rid of warnings as
-well.
-
-Have a look at the paper by http://www.covingtoninnovations.com/mc/plcoding.pdf[Covington et al.] on Prolog coding guidelines.
-
-Concerning naming of identifiers: try to use names for constants,
-functors and predicates that are unique and not a prefix of other names.
-This ensures that one can quickly find all uses/definitions with grep or
-BBEdit.
-
-[[module-information]]
-Module Information
-------------------
-
-Every module should be annotated with module information. This is used
-by our coverage analysis tool.
-
-....
-:- module(MYMODULE, [ exported_predicate/arity, ... ]).
-
-:- use_module(tools).
-
-:- module_info(group,kernel).
-:- module_info(description,'This module does wonderful things').
-....
-
-[[unit-tests]]
-Unit Tests
-----------
-
-Unit tests should be setup using the self_check module.
-
-....
-:- use_module(self_check).
-....
-
-Afterwards you can use the following to add new unit tests:
-
-....
-:- assert_must_succeed((bsets_clp:empty_sequence([]))).
-:- assert_must_fail((bsets_clp:empty_sequence([int(1)]))).
-....
-
-These tests can be run manually from the ProB Tcl/Tk version, from the
-command-line using the -self_check command. They will also be
-automatically run on our jenkins server after committing.
-
-[[errors]]
-Errors
-------
-
-Errors should be raised using one of the `add_error` predicates in the
-`error_manager` module. This will ensure that the errors are brought to
-the attention of the user in an appropriate way, depending on whether
-the Rodin, the Tcl/Tk, the command-line version is run and also
-depending on whether the tool is in testing and/or batch mode.
-
-NOTE: For internal errors that should never occur use the
-`add_internal_error` predicate. This ensures that the
-https://www3.hhu.de/stups/internal/coverage/html/[coverage information]
-is shown accordingly (in blue rather than red in the highlighting and
-this also affects coverage statistics).
-
-[[preferences-for-coding-guidelines]]
-Preferences
------------
-
-Preferences should be declared in the `preferences` module. Each
-preference must have a default value, a textual description, a type and
-category. Optionally, a short string for setting the preference from the
-command-line can be given (using the `-p PREF VALUE` switch).
-
-[[git]]
-Git
----
-
-* before committing ensure that probcli can be built (make prob);
-otherwise git bisect gets annoying to use (one can use git bisect skip
-to some extent, but it is annoying)
-* run integration tests before pushing your changes (ideally also before
-committing to avoid later issues with git bisect); ideally you should
-run as many tests as possible, but at least those affecting the parts
-you have changed. See alias below to start the test REPL. The command
-"test" then starts the ProB Test REPL. Type something like "tickets"
-to run all non-regression tests related to tickets.
-* as a rule of thumb: use rebase before pushing your changes to gitlab,
-especially when you only have one real commit.
-* avoid merge bombs with many changed files: a Git merge can hide unintended changes,
-e.g., accidentally reverting previous commits because of editor issues (editor out of sync with file system).
-* provide good commit messages. If a commit is related to a JIRA ticket
-reference the identifier of the ticket in the commit message.
-https://chris.beams.io/posts/git-commit/[This web page] provides the following seven rules:
- * Separate subject from body with a blank line
- * Limit the subject line to 50 characters
- * Capitalize the subject line
- * Do not end the subject line with a period
- * Use the imperative mood in the subject line
- * Wrap the body at 72 characters
- * Use the body to explain what and why vs. how
-
-
-[[useful-bash-aliases]]
-Useful Bash Aliases
--------------------
-
-To run probcli from sources:
-
-`alias probsli='rlwrap sicstus -l $PROB_SOURCE_DIR/prob_cli.pl --goal "go_cli." -a'`
-
-To run probcli with the REPL from sources:
-
-`alias seval='cd $NEWPROBDIR; rlwrap sicstus -l $PROB_SOURCE_DIR/prob_cli.pl --goal "go_cli." -a -repl -init -p WARN_WHEN_EXPANDING_INFINITE_CLOSURES 0 -p CLPFD TRUE'`
-
-To run ProB Tcl/Tk from sources:
-
-`alias prob='cd $PROB_SOURCE_DIR; unlimit; sics -Dprob_profile=true -l $PROB_SOURCE_DIR/prob_tcltk.pl --goal "go."'`
-
-To run the ProB Test REPL from sources:
-
-`alias test='cd $PROB_SOURCE_DIR/..; rlwrap sicstus -Dprob_safe_mode=true -l $PROB_SOURCE_DIR/test_runner.pl --goal "test_repl."'`
diff --git a/src/docs/chapter/user/52_Prolog/Running_ProB_from_source.adoc b/src/docs/chapter/user/52_Prolog/Running_ProB_from_source.adoc
deleted file mode 100644
index f9eb4fd..0000000
--- a/src/docs/chapter/user/52_Prolog/Running_ProB_from_source.adoc
+++ /dev/null
@@ -1,66 +0,0 @@
-
-[[running-prob-from-source]]
-= Running ProB from source
-
-[[getting-prob-sources]]
-== Getting the sources
-
-You can download the latest Prolog sourcecode snapshot from: [http://www3.hhu.de/stups/downloads/prob/source/ http://www3.hhu.de/stups/downloads/prob/source/]
-
-
-You may also wish to obtain related Java sources:
-* The source code for the ProB parsers (B, LTL, ...) can be obtained from: [https://https://github.com/hhu-stups/probparsers https://github.com/hhu-stups/probparsers].
-* The ProB2-Java-API source code can be obtained from: [https://github.com/hhu-stups/prob2_kernel https://github.com/hhu-stups/prob2_kernel].
-* The ProB2-Java-FX UI source code can be obtained from: [https://github.com/hhu-stups/prob2_ui https://github.com/hhu-stups/prob2_ui].
-* The B to Java value translator can also be useful and is a separate project: [https://github.com/hhu-stups/value-translator https://github.com/hhu-stups/value-translator].
-* The Plugin for Rodin is also a separate project: [https://github.com/hhu-stups/prob-rodinplugin https://github.com/hhu-stups/prob-rodinplugin].
-* The Alloy to B translator is here: [https://github.com/hhu-stups/alloy2b https://github.com/hhu-stups/alloy2b].
-
-[[starting-prob-tcltk]]
-== Starting ProB Tcl/Tk
-
-Go into the prob_prolog directory and type:
-
-`sicstus -Dprob_profile=true -l src/prob_tcltk.pl --goal "go."'`
-
-[[starting-probcli-command-line-version]]
-== Starting probcli command-line version
-
-To start probcli from source define this alias, where `SICSTUSDIR` must
-be defined:
-
-`alias probsli='rlwrap $SICSTUSDIR/bin/sicstus -l src/prob_cli.pl --goal "go_cli." -a'`
-
-You can now use probsli just like probcli, e.g.,
-
-`probsli M.mch --model-check`
-
-[[running-prob-tests-from-source]]
-== Running ProB tests from source
-
-Starting test runner from source: First define the alias, where
-`PROBDIR` and `SICSTUSDIR` must be defined:
-
-`alias tests='cd $PROBDIR; rlwrap $SICSTUSDIR/bin/sicstus -Dprob_safe_mode=true -l $PROBDIR/src/test_runner.pl --goal "test_repl."-- '`
-
-Now you can start the test runner like this:
-
-`tests`
-
-or you can already specify tests to be run:
-
-`tests last`
-
-[[prob-prolog-compile-time-flags]]
-== ProB Prolog compile time flags
-
-By giving sicstus a command-line option `-Dflag=true` you can set
-certain compile time flags, namely:
-
-`prob_profile (enables B operation profiling to be displayed in ProB Tcl/Tk in Debug menu)` +
-`prob_safe_mode (performs additional checking, in particular that ASTs are well-formed)` +
-`prob_data_validation_mode (deprecated, replaced by DATA_VALIDATION preference)` +
-`prob_release (removes certain tests from the code)` +
-`no_terminal_colors (disable terminal colors)` +
-`debug_kodkod (write dot files for kodkod interval analysis)` +
-`no_wd_checking (disable WD checking for function application)`
diff --git a/src/docs/chapter/user/52_Prolog/Why_Prolog.adoc b/src/docs/chapter/user/52_Prolog/Why_Prolog.adoc
deleted file mode 100644
index bbde80b..0000000
--- a/src/docs/chapter/user/52_Prolog/Why_Prolog.adoc
+++ /dev/null
@@ -1,364 +0,0 @@
-
-[[why-prolog]]
-= Why Prolog?
-
-In this chapter we try to answer the question: why did we use Prolog to develop
-the core of ProB, and in particular why do we use the commercial
-https://www.sics.se/projects/sicstus-prolog-leading-prolog-technology[SICStus Prolog] rather
-than an open-source alternative.
-
-The short answer is that Prolog allows us to flexibly implement various
-specification formalisms as well as the analysis and verification tools
-that go along with it. At the same time, Prolog is very fast and SICStus
-Prolog is one of the fastest and most stable Prolog systems, allows
-access to more than 256 MB of heap even on 32 bit systems (important for
-model checking), and is easy to interate with other programming
-languages (so that the GUI does not have to be developed in Prolog).
-
-[[but-why-prolog]]
-== But why Prolog?
-
-* Prolog is a convenient language in which to express the semantics of
-other languages.
-
-::
- In particular, high-level languages with non-determinism can be
- expressed with an ease that is hard to match by other languages. For
- example, the ProB source code to encode the semantics of the internal
- choice (encoded internally as '|') from CSP is basically as follows:
-
-....
-cspm_trans('|'(X,_Y),tau,X).
-cspm_trans('|'(_X,Y),tau,Y).
-....
-
-::
- The full operational semantics of CSP from Roscoe's book has been
- translated mostly one-to-one into Prolog rules (adding treatment for
- source location information,...).
-
-* Prolog is (one of) the most convenient languages to express program
-analysis
-
-::
- (e.g., abstract interpretation or even dataflow analysis, see also
- last chapters of 2nd edition of the Dragon book), program verification
- (e.g., model checking), and program transformation (e.g., partial
- evaluation) in. Also, type inference and type checking are a
- "breeze" thanks to Prolog's unification.
-
-* Modern Prolog systems support a feature called "co-routining",
-
-::
- also known as flexible computation rules or delay-declarations. These
- can be implemented by block-declarations or when-statements and they
- can stipulate conditions under which a Prolog goal should be expanded.
- For example, the following block declarations say that the goal
- less_than_equal should only be expanded when both of its arguments are
- known:
-
-....
-:- block less_than_equal(-,?), less_than_equal(?,-).
-less_than_equal(X,Y) :- X=<Y.
-....
-
-::
- A nice aspect is that the block declarations do *not* influence the
- declarative semantics of a Prolog program because of the theorem which
- states that the declarative semantics of logic programs is independent
- of the selection rule.
-
-I believe this to be one of the "killer" features of modern Prolog
-systems. We heavily use this in the ProB kernel to delay enumeration of
-values and to implement our own constraint solver over sets and
-relations. In my experience, this feature allows one to write much more
-declarative code than with traditional Prolog systems (an example is the
-transcription of Roscoe's operational semantics mentioned above), while
-often obtaining a dramatic increase in performance in generate-and-test
-scenarios.
-
-* Prolog is fast.
-
-::
- This may be surprising to some as Prolog sometimes has a reputation of
- being slow. On the laptop used for the experiments below, SICStus
- Prolog can perfrom 33 Million logical inferences per second (on my
- very latest laptop in can actually perform 75 Million logical
- inferences per second in 64-bit mode). As you see below, it can
- sometimes be faster than Java. Modern Prolog systems are well tuned
- and developed, and will outperform your own logical inference or
- unification mechanism by a considerable margin (I observed a factor of
- 10,000 between SICStus Prolog and the C implementation of a custom
- rule engine in a commercial product).
-
-In summary, Prolog gives us both a flexible way to encode both the
-operational semantics of many high-level formalisms (B, Z, CSP, ...) and
-various flexible tools on top such as animation, type checking, model
-checking and refinement checking.
-
-All of this comes with a respectable performance, despite the
-flexibility of the approach.
-
-There are of course still aspects with Prolog that, despite many years
-of research and development, are not ideal. Standardisation of Prolog
-and the libraries is not ideal (the ISO standard does not cover the
-module system for one). There is no standard static type checking tool.
-
-[[why-sicstus-prolog]]
-== Why SICStus Prolog
-
-Below is a short summary of some of the Prolog systems that to my
-knowledge are still being actively maintained (please email me
-corrections and additions).
-
-SICStus:
-
-* + Fast, good support
-* + Standalone binaries
-* + >256 MB Heap on 32 Bit systems
-* + C, Java, TclTk external interfaces,
-* + Good libraries (from Quintus)
-* + fast co-routines and constraint solving
-* - commercial product (with academic site licences available)
-* - no multi-threading
-
-SWI
-
-* + Actively maintained
-* + Large number of libraries and features
-* + Support for co-routines and constraint solving
-* - still slow
-
-Ciao
-
-* + comes with CiaoPP analyser for static analysis
-* + good module system
-* + relatively fast
-* + decent support for co-routines and constraint solving
-* - Long startup time
-
-Gnu Prolog
-
-* + good Constraint solving
-* - No co-routines
-* - limited features and libraries
-* - no BigInts
-
-XSB Prolog:
-
-* + Tabling
-* + Prolog facts can be used as efficient relational database
-* - non-standard built-ins (no print, ... quite ≠ from SWI, ...)
-* - no co-routines nor constraint solving
-* - no BigInts
-
-Yap
-
-* + fast
-* - no finite domain constraint solver
-* - no BigInts
-* - only C external language interface
-
-LPA
-
-* + good graphical tools, GUI generation, ...
-* - runs only Windows
-* - no modules
-* - no co-routines
-
-BinProlog
-
-* - no Bigints
-* - commercial
-
-B Prolog
-
-* - no Bigints prior to version 7.6, but now available
-* + constraint-based graphics library
-* - commercial (but free academic license)
-* + has action-rule mechanism (which apparently is a co-routining
-mechanism; I have not yet been able to experiment with it)
-
-Other Prologs with which I have not directly experimented are: Visual
-Prolog and IF Prolog.
-
-It seems that maybe Yap and SWI are merging efforts. It would be nice to
-have a Prolog system with the features of SWI and the speed of YAP. This
-would be a serious (free) alternative to SICStus Prolog.
-
-[[a-small-benchmark]]
-== A small benchmark
-
-Below I have conducted a small experiment to gauge the performance of
-various Prolog systems. I do not claim that this example is
-representative; it tests only a few aspects of performance (e.g., speed
-of recursive calls). I don't have the time to do a more extensive
-evaluation at the moment.
-
-The benchmark is the Fibonacci function written in the naive recursive
-way so as to quickly obtain a large number of recursive calls. The
-advantage is that the code can be easily transcribed into other
-programming languages. Below, I give you also a Python, a Haskell, and a
-Java version using BigInts. The benchmarks were run on a MacBook Pro
-Core2 Duo with 2.33 GHz. BinProlog does not have a demo licence for Mac;
-hence I had to run the Windows version in Parallels. LPA Prolog only
-runs on Windows; so it was also run using Parallels.
-
-NOTE: the purpose of the benchmark was to measure the performance of recursion. As such, I
-was trying to use the same types of data on all platforms (BigInts).
-Also note that this is actually not a typical Prolog "application" as
-no use is made of unification or non-determinism. But it is a good
-application for a functional programming language such as Haskell since
-Fibonacci is a pure function without side-effects.
-
-Also, I do not claim that the benchmark shows that Prolog is faster than
-Java in general. My only claim is that if an application is well suited
-to Prolog, its performance can be surprisingly good. I also have the
-feeling that Haskell has made great strides in performance recently, and
-that the Prolog community should be on its guard (so as not to be left
-behind).
-
-....
-System BigInts Fib(30) Fib(35)
-Java 1.5.0_16 NO (long) 0.020 0.231
-GHC 6.10.1 yes 0.082 0.878
-Yap 5.1.3 NO 0.193 2.112
-SICStus 4.0.4 yes 0.240 2.640
-Ciao 1.13.0 yes 0.312 3.461
-BinProlog 11.38 NO 0.361 3.725
-Java 1.5.0_16 yes 0.445 4.898
-XSB 3.1 NO 0.456 5.064
-Python 2.5.1 yes 0.760 8.350
-Gnu 1.3.1 NO 1.183 13.139
-SWI 5.6.52 yes 1.900 20.990
-LPA 4.710 yes 1.736 36.250
-....
-
-The same table with only the BigInteger versions is:
-
-....
-System BigInts Fib(30) Fib(35)
-GHC 6.10.1 yes 0.082 0.878
-SICStus 4.0.4 yes 0.240 2.640
-Ciao 1.13.0 yes 0.312 3.461
-Java 1.5.0_16 yes 0.445 4.898
-Python 2.5.1 yes 0.760 8.350
-SWI 5.6.52 yes 1.900 20.990
-LPA 4.710 yes 1.736 36.250
-....
-
-I have also recently tested B Prolog 7.4. It seems to perform marginally
-faster than SICStus (3 %), but does not support BigInts. Note, that Gnu
-is the only system requiring tweaking of parameters:
-
-....
-export TRAILSZ=200000
-export GLOBALSZ=1500000
-....
-
-Java with int rather than BigIntegers takes 0.016 s for Fib(30) and
-0.163 s for Fib(35). Note that GHC Haskell seems to have received a big
-performance boost on this particular example (earlier versions of
-Haskell were on par with SICStus Prolog).
-
-I also wanted to experiment with a Mercury version, but for the moment
-Mercury does not compile/install on my machine. Marc Fontaine has also
-written various Haskell versions of Fibonacci
-
-Here are the various versions of Fibonacci:
-
-Prolog Version:
-
-....
-fib(0,1) :- !.
-fib(1,1) :- !.
-fib(N,R) :-
- N1 is N-1, N2 is N1-1, fib(N1,R1), fib(N2,R2),
- R is R1+R2.
-....
-
-Python Version:
-
-....
-def Fib(x):
- if x<2:
- return 1
- else:
- return Fib(x-1)+Fib(x-2)
-....
-
-Java Version with BigInteger:
-
-....
-private static BigInteger ZERO = BigInteger.ZERO;
-private static BigInteger ONE = BigInteger.ONE;
-private static BigInteger TWO = new BigInteger("2");
-public static BigInteger naiveFib(BigInteger x) {
- if (x.equals(ZERO) ) return ONE;
- if (x.equals(ONE) ) return BigInteger.ONE;
- return naiveFib(x.subtract(ONE)).add(naiveFib(x.subtract(TWO)));
-}
-....
-
-Haskell Version:
-
-....
-fib :: Integer -> Integer
-fib n
- | n == 0 = 1
- | n == 1 = 1
- | otherwise = fib(n-1) + fib(n-2)
-....
-
-Java Version with long rather than BigIntegers:
-
-....
-public static long fib(long xx) {
- if (xx<2)
- return 1;
- else
- return fib(xx-1)+fib(xx-2);
-}
-....
-
-[[startup-times]]
-== Startup Times
-
-Below we test the startup times of some of the Prolog systems.
-Unfortunately, not all Prolog systems can easily be started as easily
-from the command-line as SICStus Prolog (e.g., --goal "GOAL."
-parameter and -l FILE parameter).
-
-First, the following command takes 0.026 s real time (0.015 s user time)
-with SICStus Prolog 4.0.5 on the same system as above:
-
-`time sicstus --goal "halt."`
-
-For SWI Prolog 5.6.64, we get 0.015 s real time (0.008 s user time):
-
-`time swipl -g "halt."`
-
-For Ciao Prolog 1.13.0-8334, we get 0.271 s user time for "time ciao"
-and then typing halt (I found no easy way to provide goals on the
-command-line).
-
-Now, take the file halt.pl with contents:
-
-....
-main :- print(hello),nl,halt.
- :- main.
-....
-
-The following takes 0.028 seconds real time and 0.015 seconds user time.
-
-`time sicstus -l halt.pl`
-
-The following takes 0.204 seconds real time the first time and 0.015
-seconds real time the second time:
-
-`time swipl -c halt.pl`
-
-The following takes 0.726 seconds real time and 0.648 seconds user time
-(after commenting out :- main.), i.e., 25 times slower than SICStus:
-
-`time ciao -c halt.pl`
diff --git a/src/docs/chapter/user/52_Prolog/ZZ_section_footer.adoc b/src/docs/chapter/user/52_Prolog/ZZ_section_footer.adoc
deleted file mode 100644
index 909c09e..0000000
--- a/src/docs/chapter/user/52_Prolog/ZZ_section_footer.adoc
+++ /dev/null
@@ -1,2 +0,0 @@
-
-:leveloffset: -1
--
GitLab