LPCIC · gares · Dec 30, 2022 · Jan 2, 2023 · Jan 2, 2023 · Jan 3, 2023
diff --git a/CHANGES.md b/CHANGES.md
@@ -1,3 +1,9 @@
+# UNRELEASED
+
+- Command line:
+  - Deprecate `-test`
+  - New `-main` to run `main` (with no arguments)
+
 # v1.16.8 (November 2022)
 
 Requires Menhir 20211230 and OCaml 4.08 or above.

diff --git a/Makefile b/Makefile
@@ -20,6 +20,11 @@ help:
 	@echo '  menhir-complete-errormsgs run when updating the grammar'
 	@echo '  menhir-strip-errormsgs remove comments from error message file'
 	@echo
+	@echo 'Doc and release targets:'
+	@echo
+	@echo '  doc-build      builds all doc in docs/build/'
+	@echo '  release        calls dune-release and uploads the doc'
+	@echo
 
 INSTALL=_build/install/default
 BUILD=_build/default

diff --git a/docs/base/cmdline.rst b/docs/base/cmdline.rst
@@ -0,0 +1,49 @@
+Running a program
+=================
+
+The :console:`elpi` command line utility can run a query against a program.
+The standard query is :elpi:`main` for which one can use the dedicated
+command line option :console:`-main`.
+
+.. elpi:: cmdline_example.elpi
+   :nostderr:
+
+Custom entry point
+++++++++++++++++++
+
+.. elpi:: cmdline_example.elpi
+   :cmdline: -exec mypred -- 1 a "hi there"
+   :nostderr:
+   :nocode:
+
+Interactive use
++++++++++++++++
+
+.. elpi:: cmdline_interactive.elpi
+   :cmdline:
+
+Typing :elpi:`guess X.` followed by enter runs the query.
+
+.. elpi:: cmdline_interactive.elpi
+   :stdin: guess X.\ny\n
+   :nostderr:
+   :cmdline:
+   :nocode:
+
+Command line options
+====================
+
+.. elpi::
+   :cmdline: -h
+
+Debug parsing
++++++++++++++
+
+.. elpi::
+   :stdin: a ++-> b **? c
+   :cmdline: -parse-term
+   :nocode:
+
+Tracing options
++++++++++++++++
+
diff --git a/docs/base/cmdline_example.elpi b/docs/base/cmdline_example.elpi
@@ -0,0 +1,4 @@
+pred mypred i:list string.
+mypred Args :- print Args.
+
+main :- print "Hello world!".
diff --git a/docs/base/cmdline_interactive.elpi b/docs/base/cmdline_interactive.elpi
@@ -0,0 +1,3 @@
+pred guess o:int.
+guess 46.
+guess 42.
diff --git a/docs/base/index.rst b/docs/base/index.rst
@@ -6,12 +6,12 @@
 Welcome to Elpi's documentation!
 ================================
 
-.. .. toctree:
-..    :maxdepth: 2
-..    :caption: Contents:
-.. 
-..    about
-..    playground
+.. toctree::
+   :maxdepth: 2
+   :caption: Usage:
+
+   cmdline
+   trace-browser
 
 .. toctree::
    :maxdepth: 2

diff --git a/docs/base/playground.rst b/docs/base/playground.rst
@@ -79,151 +79,142 @@ Regexp Matching
 
 This ``elpi`` directive should pass validation:
 
-.. code-block:: console
-
-   .. elpi:: ./a.elpi
-      :assert: V = s \(.*\)
-
 .. elpi:: ./a.elpi
    :assert: V = s \(.*\)
+   :nostderr:
 
 This one should fail validation, only a message stating the regexp matching error will be printed:
 
-.. code-block:: console
-
-   .. elpi:: ./a.elpi
-      :assert: /(?!)/
-
-.. elpi:: ./a.elpi
-   :assert: /(?!)/
+.. .. elpi:: ./a.elpi
+..    :assert: /(?!)/
 
 Test Bed
 --------
 
 .. elpi:: ../../tests/sources/accumulate_twice1.elpi
-.. elpi:: ../../tests/sources/accumulate_twice2.elpi
-.. elpi:: ../../tests/sources/accumulated.elpi
-.. elpi:: ../../tests/sources/ackermann.elpi
-.. elpi:: ../../tests/sources/asclause.elpi
-.. elpi:: ../../tests/sources/beta.elpi
-.. elpi:: ../../tests/sources/block.elpi
-.. elpi:: ../../tests/sources/chr.elpi
-.. elpi:: ../../tests/sources/chrGCD.elpi
-.. elpi:: ../../tests/sources/chrLEQ.elpi
-.. elpi:: ../../tests/sources/chr_nokey.elpi
-.. elpi:: ../../tests/sources/chr_nokey2.elpi
-.. elpi:: ../../tests/sources/chr_not_clique.elpi
-.. elpi:: ../../tests/sources/chr_sem.elpi
-.. elpi:: ../../tests/sources/conj2.elpi
-.. elpi:: ../../tests/sources/ctx_loading.elpi
-.. elpi:: ../../tests/sources/cut.elpi
-.. elpi:: ../../tests/sources/cut2.elpi
-.. elpi:: ../../tests/sources/cut3.elpi
-.. elpi:: ../../tests/sources/cut4.elpi
-.. elpi:: ../../tests/sources/cut5.elpi
-.. elpi:: ../../tests/sources/cut6.elpi
-.. elpi:: ../../tests/sources/deep_indexing.elpi
-.. elpi:: ../../tests/sources/discard.elpi
-.. elpi:: ../../tests/sources/elpi_only_llam.elpi
-.. elpi:: ../../tests/sources/end_comment.elpi
-.. elpi:: ../../tests/sources/eta.elpi
-.. elpi:: ../../tests/sources/eta_as.elpi
-.. elpi:: ../../tests/sources/even-odd.elpi
-.. elpi:: ../../tests/sources/findall.elpi
-.. elpi:: ../../tests/sources/fragment_exit.elpi
-.. elpi:: ../../tests/sources/fragment_exit2.elpi
-.. elpi:: ../../tests/sources/fragment_exit3.elpi
-.. elpi:: ../../tests/sources/general_case.elpi
-.. elpi:: ../../tests/sources/general_case2.elpi
-.. elpi:: ../../tests/sources/general_case3.elpi
-.. elpi:: ../../tests/sources/hc_interp.elpi
-.. elpi:: ../../tests/sources/hdclause.elpi
-.. elpi:: ../../tests/sources/heap_discard.elpi
-.. elpi:: ../../tests/sources/ho.elpi
-.. elpi:: ../../tests/sources/hollight.elpi
-.. elpi:: ../../tests/sources/hollight_legacy.elpi
-.. elpi:: ../../tests/sources/hyp_uvar.elpi
-.. elpi:: ../../tests/sources/impl.elpi
-.. elpi:: ../../tests/sources/impl2.elpi
-.. elpi:: ../../tests/sources/index2.elpi
-.. elpi:: ../../tests/sources/io_colon.elpi
-.. elpi:: ../../tests/sources/lambda.elpi
-.. elpi:: ../../tests/sources/lambda2.elpi
-.. elpi:: ../../tests/sources/lambda3.elpi
-.. elpi:: ../../tests/sources/list_as_conj.elpi
-.. elpi:: ../../tests/sources/list_comma.elpi
-.. elpi:: ../../tests/sources/llam.elpi
-.. elpi:: ../../tests/sources/llamchr.elpi
-.. elpi:: ../../tests/sources/map.elpi
-.. elpi:: ../../tests/sources/map_list.elpi
-.. elpi:: ../../tests/sources/map_list_opt.elpi
-.. elpi:: ../../tests/sources/name_builtin.elpi
-.. elpi:: ../../tests/sources/named_clauses00.elpi
-.. elpi:: ../../tests/sources/named_clauses01.elpi
-.. elpi:: ../../tests/sources/named_clauses02.elpi
-.. elpi:: ../../tests/sources/namespaces00.elpi
-.. elpi:: ../../tests/sources/namespaces01.elpi
-.. elpi:: ../../tests/sources/namespaces02.elpi
-.. elpi:: ../../tests/sources/namespaces03.elpi
-.. elpi:: ../../tests/sources/nil_cons.elpi
-.. elpi:: ../../tests/sources/notation.elpi
-.. elpi:: ../../tests/sources/notation_error.elpi
-.. elpi:: ../../tests/sources/notation_legacy.elpi
-.. elpi:: ../../tests/sources/patternunif.elpi
-.. elpi:: ../../tests/sources/patternunif2.elpi
-.. elpi:: ../../tests/sources/pi.elpi
-.. elpi:: ../../tests/sources/pi3.elpi
-.. elpi:: ../../tests/sources/pi5.elpi
-.. elpi:: ../../tests/sources/pnf.elpi
-.. elpi:: ../../tests/sources/polymorphic_variants.elpi
-.. elpi:: ../../tests/sources/printer.elpi
-.. elpi:: ../../tests/sources/queens.elpi
-.. elpi:: ../../tests/sources/quote_syntax.elpi
-.. elpi:: ../../tests/sources/random.elpi
-.. elpi:: ../../tests/sources/reduce_cbn.elpi
-.. elpi:: ../../tests/sources/reduce_cbv.elpi
-.. elpi:: ../../tests/sources/restriction.elpi
-.. elpi:: ../../tests/sources/restriction3.elpi
-.. elpi:: ../../tests/sources/restriction4.elpi
-.. elpi:: ../../tests/sources/restriction5.elpi
-.. elpi:: ../../tests/sources/restriction6.elpi
-.. elpi:: ../../tests/sources/rev.elpi
-.. elpi:: ../../tests/sources/rev14.elpi
-.. elpi:: ../../tests/sources/same_term.elpi
-.. elpi:: ../../tests/sources/self_assignment.elpi
-.. elpi:: ../../tests/sources/set.elpi
-.. elpi:: ../../tests/sources/shorten.elpi
-.. elpi:: ../../tests/sources/shorten2.elpi
-.. elpi:: ../../tests/sources/shorten_aux.elpi
-.. elpi:: ../../tests/sources/shorten_aux2.elpi
-.. elpi:: ../../tests/sources/shorten_builtin.elpi
-.. elpi:: ../../tests/sources/shorten_trie.elpi
-.. elpi:: ../../tests/sources/spill_and.elpi
-.. elpi:: ../../tests/sources/spill_impl.elpi
-.. elpi:: ../../tests/sources/spill_lam.elpi
-.. elpi:: ../../tests/sources/trace.elpi
-.. elpi:: ../../tests/sources/trace2.elpi
-.. elpi:: ../../tests/sources/trace_chr.elpi
-.. elpi:: ../../tests/sources/trace_cut.elpi
-.. elpi:: ../../tests/sources/trace_findall.elpi
-.. elpi:: ../../tests/sources/trail.elpi
-.. elpi:: ../../tests/sources/typeabbrv.elpi
-.. elpi:: ../../tests/sources/typeabbrv1.elpi
-.. elpi:: ../../tests/sources/typeabbrv10.elpi
-.. elpi:: ../../tests/sources/typeabbrv11.elpi
-.. elpi:: ../../tests/sources/typeabbrv12.elpi
-.. elpi:: ../../tests/sources/typeabbrv2.elpi
-.. elpi:: ../../tests/sources/typeabbrv3.elpi
-.. elpi:: ../../tests/sources/typeabbrv4.elpi
-.. elpi:: ../../tests/sources/typeabbrv5.elpi
-.. elpi:: ../../tests/sources/typeabbrv6.elpi
-.. elpi:: ../../tests/sources/typeabbrv7.elpi
-.. elpi:: ../../tests/sources/typeabbrv8.elpi
-.. elpi:: ../../tests/sources/typeabbrv9.elpi
-.. elpi:: ../../tests/sources/uminus.elpi
-.. elpi:: ../../tests/sources/uvar_chr.elpi
-.. elpi:: ../../tests/sources/var.elpi
-.. elpi:: ../../tests/sources/variadic_declare_constraints.elpi
-.. elpi:: ../../tests/sources/w.elpi
-.. elpi:: ../../tests/sources/w_legacy.elpi
-.. elpi:: ../../tests/sources/zebra.elpi
+.. .. elpi:: ../../tests/sources/accumulate_twice2.elpi
+.. .. elpi:: ../../tests/sources/accumulated.elpi
+.. .. elpi:: ../../tests/sources/ackermann.elpi
+.. .. elpi:: ../../tests/sources/asclause.elpi
+.. .. elpi:: ../../tests/sources/beta.elpi
+.. .. elpi:: ../../tests/sources/block.elpi
+.. .. elpi:: ../../tests/sources/chr.elpi
+.. .. elpi:: ../../tests/sources/chrGCD.elpi
+.. .. elpi:: ../../tests/sources/chrLEQ.elpi
+.. .. elpi:: ../../tests/sources/chr_nokey.elpi
+.. .. elpi:: ../../tests/sources/chr_nokey2.elpi
+.. .. elpi:: ../../tests/sources/chr_not_clique.elpi
+.. .. elpi:: ../../tests/sources/chr_sem.elpi
+.. .. elpi:: ../../tests/sources/conj2.elpi
+.. .. elpi:: ../../tests/sources/ctx_loading.elpi
+.. .. elpi:: ../../tests/sources/cut.elpi
+.. .. elpi:: ../../tests/sources/cut2.elpi
+.. .. elpi:: ../../tests/sources/cut3.elpi
+.. .. elpi:: ../../tests/sources/cut4.elpi
+.. .. elpi:: ../../tests/sources/cut5.elpi
+.. .. elpi:: ../../tests/sources/cut6.elpi
+.. .. elpi:: ../../tests/sources/deep_indexing.elpi
+.. .. elpi:: ../../tests/sources/discard.elpi
+.. .. elpi:: ../../tests/sources/elpi_only_llam.elpi
+.. .. elpi:: ../../tests/sources/end_comment.elpi
+.. .. elpi:: ../../tests/sources/eta.elpi
+.. .. elpi:: ../../tests/sources/eta_as.elpi
+.. .. elpi:: ../../tests/sources/even-odd.elpi
+.. .. elpi:: ../../tests/sources/findall.elpi
+.. .. elpi:: ../../tests/sources/fragment_exit.elpi
+.. .. elpi:: ../../tests/sources/fragment_exit2.elpi
+.. .. elpi:: ../../tests/sources/fragment_exit3.elpi
+.. .. elpi:: ../../tests/sources/general_case.elpi
+.. .. elpi:: ../../tests/sources/general_case2.elpi
+.. .. elpi:: ../../tests/sources/general_case3.elpi
+.. .. elpi:: ../../tests/sources/hc_interp.elpi
+.. .. elpi:: ../../tests/sources/hdclause.elpi
+.. .. elpi:: ../../tests/sources/heap_discard.elpi
+.. .. elpi:: ../../tests/sources/ho.elpi
+.. .. elpi:: ../../tests/sources/hollight.elpi
+.. .. elpi:: ../../tests/sources/hollight_legacy.elpi
+.. .. elpi:: ../../tests/sources/hyp_uvar.elpi
+.. .. elpi:: ../../tests/sources/impl.elpi
+.. .. elpi:: ../../tests/sources/impl2.elpi
+.. .. elpi:: ../../tests/sources/index2.elpi
+.. .. elpi:: ../../tests/sources/io_colon.elpi
+.. .. elpi:: ../../tests/sources/lambda.elpi
+.. .. elpi:: ../../tests/sources/lambda2.elpi
+.. .. elpi:: ../../tests/sources/lambda3.elpi
+.. .. elpi:: ../../tests/sources/list_as_conj.elpi
+.. .. elpi:: ../../tests/sources/list_comma.elpi
+.. .. elpi:: ../../tests/sources/llam.elpi
+.. .. elpi:: ../../tests/sources/llamchr.elpi
+.. .. elpi:: ../../tests/sources/map.elpi
+.. .. elpi:: ../../tests/sources/map_list.elpi
+.. .. elpi:: ../../tests/sources/map_list_opt.elpi
+.. .. elpi:: ../../tests/sources/name_builtin.elpi
+.. .. elpi:: ../../tests/sources/named_clauses00.elpi
+.. .. elpi:: ../../tests/sources/named_clauses01.elpi
+.. .. elpi:: ../../tests/sources/named_clauses02.elpi
+.. .. elpi:: ../../tests/sources/namespaces00.elpi
+.. .. elpi:: ../../tests/sources/namespaces01.elpi
+.. .. elpi:: ../../tests/sources/namespaces02.elpi
+.. .. elpi:: ../../tests/sources/namespaces03.elpi
+.. .. elpi:: ../../tests/sources/nil_cons.elpi
+.. .. elpi:: ../../tests/sources/notation.elpi
+.. .. elpi:: ../../tests/sources/notation_error.elpi
+.. .. elpi:: ../../tests/sources/notation_legacy.elpi
+.. .. elpi:: ../../tests/sources/patternunif.elpi
+.. .. elpi:: ../../tests/sources/patternunif2.elpi
+.. .. elpi:: ../../tests/sources/pi.elpi
+.. .. elpi:: ../../tests/sources/pi3.elpi
+.. .. elpi:: ../../tests/sources/pi5.elpi
+.. .. elpi:: ../../tests/sources/pnf.elpi
+.. .. elpi:: ../../tests/sources/polymorphic_variants.elpi
+.. .. elpi:: ../../tests/sources/printer.elpi
+.. .. elpi:: ../../tests/sources/queens.elpi
+.. .. elpi:: ../../tests/sources/quote_syntax.elpi
+.. .. elpi:: ../../tests/sources/random.elpi
+.. .. elpi:: ../../tests/sources/reduce_cbn.elpi
+.. .. elpi:: ../../tests/sources/reduce_cbv.elpi
+.. .. elpi:: ../../tests/sources/restriction.elpi
+.. .. elpi:: ../../tests/sources/restriction3.elpi
+.. .. elpi:: ../../tests/sources/restriction4.elpi
+.. .. elpi:: ../../tests/sources/restriction5.elpi
+.. .. elpi:: ../../tests/sources/restriction6.elpi
+.. .. elpi:: ../../tests/sources/rev.elpi
+.. .. elpi:: ../../tests/sources/rev14.elpi
+.. .. elpi:: ../../tests/sources/same_term.elpi
+.. .. elpi:: ../../tests/sources/self_assignment.elpi
+.. .. elpi:: ../../tests/sources/set.elpi
+.. .. elpi:: ../../tests/sources/shorten.elpi
+.. .. elpi:: ../../tests/sources/shorten2.elpi
+.. .. elpi:: ../../tests/sources/shorten_aux.elpi
+.. .. elpi:: ../../tests/sources/shorten_aux2.elpi
+.. .. elpi:: ../../tests/sources/shorten_builtin.elpi
+.. .. elpi:: ../../tests/sources/shorten_trie.elpi
+.. .. elpi:: ../../tests/sources/spill_and.elpi
+.. .. elpi:: ../../tests/sources/spill_impl.elpi
+.. .. elpi:: ../../tests/sources/spill_lam.elpi
+.. .. elpi:: ../../tests/sources/trace.elpi
+.. .. elpi:: ../../tests/sources/trace2.elpi
+.. .. elpi:: ../../tests/sources/trace_chr.elpi
+.. .. elpi:: ../../tests/sources/trace_cut.elpi
+.. .. elpi:: ../../tests/sources/trace_findall.elpi
+.. .. elpi:: ../../tests/sources/trail.elpi
+.. .. elpi:: ../../tests/sources/typeabbrv.elpi
+.. .. elpi:: ../../tests/sources/typeabbrv1.elpi
+.. .. elpi:: ../../tests/sources/typeabbrv10.elpi
+.. .. elpi:: ../../tests/sources/typeabbrv11.elpi
+.. .. elpi:: ../../tests/sources/typeabbrv12.elpi
+.. .. elpi:: ../../tests/sources/typeabbrv2.elpi
+.. .. elpi:: ../../tests/sources/typeabbrv3.elpi
+.. .. elpi:: ../../tests/sources/typeabbrv4.elpi
+.. .. elpi:: ../../tests/sources/typeabbrv5.elpi
+.. .. elpi:: ../../tests/sources/typeabbrv6.elpi
+.. .. elpi:: ../../tests/sources/typeabbrv7.elpi
+.. .. elpi:: ../../tests/sources/typeabbrv8.elpi
+.. .. elpi:: ../../tests/sources/typeabbrv9.elpi
+.. .. elpi:: ../../tests/sources/uminus.elpi
+.. .. elpi:: ../../tests/sources/uvar_chr.elpi
+.. .. elpi:: ../../tests/sources/var.elpi
+.. .. elpi:: ../../tests/sources/variadic_declare_constraints.elpi
+.. .. elpi:: ../../tests/sources/w.elpi
+.. .. elpi:: ../../tests/sources/w_legacy.elpi
+.. .. elpi:: ../../tests/sources/zebra.elpi
diff --git a/docs/base/trace-browser.gif b/docs/base/trace-browser.gif
diff --git a/docs/base/trace-browser.rst b/docs/base/trace-browser.rst
@@ -0,0 +1,6 @@
+Trace Browser
+=============
+
+.. image:: trace-browser.gif
+  :width: 800
+  :alt: Trace browsing in action
diff --git a/docs/base/trace-browser_example.elpi b/docs/base/trace-browser_example.elpi
@@ -0,0 +1,5 @@
+pred p i:int.
+p X :- X > 2.
+p 1.
+
+main :- p 1.