CHANGES.md

 # Changes
 
+## 2019/09/24
+
+* Build Menhir's standard library into the Menhir executable instead of
+  storing it in a separate file `standard.mly`. This removes the need to
+  hardcode the path to this file into the Menhir executable. This also
+  removes the need for the command line switch `--stdlib`, which remains
+  supported but is now ignored, and for the environment variable
+  `$MENHIR_STDLIB`, which is now ignored. (Suggested and implemented
+  by Nicolás Ojeda Bär.)
+
 ## 2019/06/20
 
 * When compiled with OCaml 4.02.3, Menhir could produce OCaml code

Makefile

@@ -52,7 +52,6 @@ libdir	        := $(PREFIX)/share/menhir
 mandir          := $(PREFIX)/share/man/man1
 MANS            := doc/menhir.1
 DOCS            := doc/manual.pdf doc/manual.html doc/manual*.png demos
-MLYLIB          := src/standard.mly
 
 # ----------------------------------------------------------------------------
 
@@ -181,7 +180,6 @@ install:
 	install $(BUILDDIR)/menhir.$(TARGET) $(bindir)/menhir$(EXE)
 # Install Menhir's standard library.
 	mkdir -p $(libdir)
-	install -m 644 $(MLYLIB) $(libdir)
 # Install MenhirLib and MenhirSdk.
 	@if `$(BUILDDIR)/menhir.$(TARGET) --suggest-ocamlfind | tr -d '\r'` ; then \
 	  echo 'Installing MenhirLib and MenhirSdk via ocamlfind.' ; \
@@ -204,7 +202,7 @@ install:
 	fi
 
 uninstall:
-	@if `$(bindir)/menhir$(EXE) --suggest-ocamlfind` ; then \
+	@if `$(bindir)/menhir$(EXE) --suggest-ocamlfind | tr -d '\r'` ; then \
 	  echo 'Un-installing MenhirLib and MenhirSdk via ocamlfind.' ; \
 	  ocamlfind remove menhirLib ; \
 	  ocamlfind remove menhirSdk ; \

check-tarball.sh

@@ -15,11 +15,9 @@ TARBALL=$PACKAGE.tar.gz
 # We use a dedicated opam switch where it is permitted to uninstall/reinstall
 # Menhir.
 
-CURRENT=`opam switch show`
-echo "The current opam switch is $CURRENT. Now switching to test-menhir..."
-opam switch test-menhir 2>/dev/null || opam switch create test-menhir 4.07.1
-eval $(opam env)
-OPAMYES=true opam install ocamlfind ocamlbuild coq
+echo "Now switching to test-menhir..."
+eval $(opam env --set-switch --switch test-menhir)
+OPAMYES=true opam install ocamlfind ocamlbuild coq dune
 
 # Uninstall Menhir if it is installed.
 
@@ -59,7 +57,7 @@ mkdir $INSTALL
 
 echo "   * Building the demos."
 (cd $TEMPDIR/$PACKAGE &&
-  make MENHIR=$INSTALL/bin/menhir -C demos
+  make MENHIR=$INSTALL/bin/menhir COQINCLUDES="-R $COQCONTRIB/MenhirLib MenhirLib" -C demos
 ) > $TEMPDIR/demos.log 2>&1 || (cat $TEMPDIR/demos.log; exit 1)
 
 echo "   * Uninstalling."
@@ -69,8 +67,3 @@ echo "   * Uninstalling."
 ) > $TEMPDIR/uninstall.log 2>&1 || (cat $TEMPDIR/uninstall.log; exit 1)
 
 rm -rf $TEMPDIR
-
-# Move back to the original switch.
-
-echo "Switching back to $CURRENT..."
-opam switch $CURRENT

coq-menhirlib/CHANGES.md

 # Changes
 
+## XXXXXXXX
+
+* Fix compatibility with Coq 8.10, and some warnings.
+
 ## 2019/06/26
 
 * Fix compatibility with Coq 8.7 and Coq 8.9:

coq-menhirlib/src/Automaton.v

@@ -99,9 +99,9 @@ Module Types(Import Init:AutInit).
                  T term = last_symb_of_non_init_state s -> lookahead_action term
   | Reduce_act: production -> lookahead_action term
   | Fail_act: lookahead_action term.
-  Arguments Shift_act [term].
-  Arguments Reduce_act [term].
-  Arguments Fail_act [term].
+  Arguments Shift_act {term}.
+  Arguments Reduce_act {term}.
+  Arguments Fail_act {term}.
 
   Inductive action :=
   | Default_reduce_act: production -> action

coq-menhirlib/src/Makefile.coq

@@ -14,7 +14,7 @@ SHELL := /usr/bin/env bash
 # ROOTDIR    (default: `pwd`)
 # COQBIN     (default: empty)
 # COQINCLUDE (default: empty)
-# V          (default: *.v)
+# VV         (default: *.v)
 # V_AUX      (default: undefined/empty)
 # SERIOUS    (default: 1)
 #            (if 0, we produce .vio files)
@@ -35,23 +35,23 @@ ifndef ROOTDIR
 	ROOTDIR := $(shell pwd)
 endif
 
-ifndef V
-	V := $(wildcard $(ROOTDIR)/*.v)
+ifndef VV
+	VV := $(wildcard $(ROOTDIR)/*.v)
 endif
 
-# Typically, $(V) should list only the .v files that we are ultimately
+# Typically, $(VV) should list only the .v files that we are ultimately
 # interested in checking. $(V_AUX) should list every other .v file in the
-# project. $(VD) is obtained from $(V) and $(V_AUX), so [make] sees all
+# project. $(VD) is obtained from $(VV) and $(V_AUX), so [make] sees all
 # dependencies and can rebuild files anywhere in the project, if needed, and
 # only if needed.
 
 ifndef VD
-	VD  := $(patsubst %.v,%.v.d,$(V) $(V_AUX))
+	VD  := $(patsubst %.v,%.v.d,$(VV) $(V_AUX))
 endif
 
-VIO := $(patsubst %.v,%.vio,$(V))
-VQ  := $(patsubst %.v,%.vq,$(V))
-VO  := $(patsubst %.v,%.vo,$(V))
+VIO := $(patsubst %.v,%.vio,$(VV))
+VQ  := $(patsubst %.v,%.vq,$(VV))
+VO  := $(patsubst %.v,%.vo,$(VV))
 
 SERIOUS := 1
 
@@ -188,7 +188,7 @@ ide: _CoqProject
 # In a multi-directory setting, it is not entirely clear how to find the
 # files that we wish to remove.
 
-# One approach would be to view $(V) as the authoritative list of source files
+# One approach would be to view $(VV) as the authoritative list of source files
 # and remove just the derived files $(VO), etc.
 
 # Another approach is to scan all subdirectories of $(ROOTDIR) and remove all

coq-menhirlib/src/Validator_classes.v

@@ -17,7 +17,7 @@ Require Import Alphabet.
 
 Class IsValidator (P : Prop) (b : bool) :=
   is_validator : b = true -> P.
-Hint Mode IsValidator + -.
+Hint Mode IsValidator + - : typeclass_instances.
 
 Instance is_validator_true : IsValidator True true.
 Proof. done. Qed.
@@ -31,7 +31,7 @@ Proof. done. Qed.
 
 Instance is_validator_and P1 b1 P2 b2 `{IsValidator P1 b1} `{IsValidator P2 b2}:
   IsValidator (P1 /\ P2) (if b1 then b2 else false).
-Proof. split; destruct b1, b2; auto using is_validator. Qed.
+Proof. by split; destruct b1, b2; apply is_validator. Qed.
 
 Instance is_validator_comparable_leibniz_eq A (C:Comparable A) (x y : A) :
   ComparableLeibnizEq C ->
@@ -49,9 +49,10 @@ Lemma is_validator_forall_finite A P b `(Finite A) :
   (forall (x : A), IsValidator (P x) (b x)) ->
   IsValidator (forall (x : A), P x) (forallb b all_list).
 Proof.
-  move=> ? /forallb_forall.
-  auto using all_list_forall, is_validator, forallb_forall.
+  move=> ? /forallb_forall Hb ?.
+  apply is_validator, Hb, all_list_forall.
 Qed.
+
 (* We do not use an instance directly here, because we need somehow to
    force Coq to instantiate b with a lambda. *)
 Hint Extern 2 (IsValidator (forall x : ?A, _) _) =>

coq-menhirlib/src/Validator_safe.v

@@ -184,8 +184,8 @@ Instance impl_is_state_valid_after_pop_is_validator state sl pl P b :
   IsValidator (state_valid_after_pop state sl pl -> P)
               (if is_state_valid_after_pop state sl pl then b else true).
 Proof.
-  destruct (is_state_valid_after_pop state0 sl pl) eqn:EQ.
-  - intros ??. auto using is_validator.
+  destruct (is_state_valid_after_pop _ sl pl) eqn:EQ.
+  - intros ???. by eapply is_validator.
   - intros _ _ Hsvap. exfalso. induction Hsvap=>//; [simpl in EQ; congruence|].
     by destruct sl.
 Qed.

coq-menhirlib/src/Version.v

@@ -12,4 +12,4 @@
 (****************************************************************************)
 
 Definition require_unreleased := tt.
-Definition require_20190626 := tt.
+Definition require_20190924 := tt.

debian/changelog

+menhir (20190924-1) unstable; urgency=medium
+
+  * New upstream version
+  * Set Multi-Arch:foreign for the menhir-doc package
+  * Standards-Version: 4.4.1 (no change)
+
+ -- Ralf Treinen <treinen@debian.org>  Sat, 02 Nov 2019 11:51:19 +0100
+
 menhir (20190626-6) unstable; urgency=medium
 
   * Team upload

debian/control

@@ -12,7 +12,7 @@ Build-Depends:
   ocaml-findlib,
   dh-ocaml,
   coq
-Standards-Version: 4.4.0
+Standards-Version: 4.4.1
 Homepage: http://gallium.inria.fr/~fpottier/menhir/
 Vcs-Browser: https://salsa.debian.org/ocaml-team/menhir
 Vcs-Git: https://salsa.debian.org/ocaml-team/menhir.git
@@ -65,6 +65,7 @@ Replaces: menhir (<< 20170712-1)
 Breaks: menhir (<< 20170712-1)
 Architecture: all
 Depends: ${misc:Depends}
+Multi-Arch: foreign
 Description: Documentation of the Menhir parser generator for OCaml
  Menhir is a LR(1) parser generator for the OCaml programming language.
  It is mostly compatible with the ocamlyacc parser generator provided with

demos/Makefile

@@ -28,6 +28,7 @@ DEMOS := \
   calc-incremental-dune \
   calc-inspection-dune \
   generate-printers-dune \
+  coq-minicalc
 
 .PHONY: all clean test
 

demos/coq-minicalc/Lexer.v

+
+(** Hand-written lexer for natural numbers, idents, parens and + - * / *)
+
+Require Import BinNat Ascii String.
+Require Import Parser.
+Import MenhirLibParser.Inter.
+Open Scope char_scope.
+Open Scope bool_scope.
+
+(** No such thing as an empty buffer, instead we use
+    an infinite stream of EOF *)
+
+CoFixpoint TheEnd : buffer := Buf_cons (EOF tt) TheEnd.
+
+Fixpoint ntail n s :=
+  match n, s with
+  | 0, _ => s
+  | _, EmptyString => s
+  | S n, String _ s => ntail n s
+  end.
+
+(** Comparison on characters *)
+
+Definition ascii_eqb c c' := (N_of_ascii c =? N_of_ascii c')%N.
+Definition ascii_leb c c' := (N_of_ascii c <=? N_of_ascii c')%N.
+
+Infix "=?" := ascii_eqb : char_scope.
+Infix "<=?" := ascii_leb : char_scope.
+
+Definition is_digit c := (("0" <=? c) && (c <=? "9"))%char.
+
+Definition is_alpha c :=
+  ((("a" <=? c) && (c <=? "z")) ||
+   (("A" <=? c) && (c <=? "Z")) ||
+   (c =? "_"))%char.
+
+Fixpoint identsize s :=
+  match s with
+  | EmptyString => 0
+  | String c s =>
+    if is_alpha c || is_digit c then S (identsize s)
+    else 0
+  end.
+
+Fixpoint readnum acc s :=
+  match s with
+  | String "0" s => readnum (acc*10) s
+  | String "1" s => readnum (acc*10+1) s
+  | String "2" s => readnum (acc*10+2) s
+  | String "3" s => readnum (acc*10+3) s
+  | String "4" s => readnum (acc*10+4) s
+  | String "5" s => readnum (acc*10+5) s
+  | String "6" s => readnum (acc*10+6) s
+  | String "7" s => readnum (acc*10+7) s
+  | String "8" s => readnum (acc*10+8) s
+  | String "9" s => readnum (acc*10+9) s
+  | _ => (acc,s)
+  end.
+
+Fixpoint lex_string_cpt n s :=
+  match n with
+  | 0 => None
+  | S n =>
+    match s with
+    | EmptyString => Some TheEnd
+    | String c s' =>
+      match c with
+      | " " => lex_string_cpt n s'
+      | "009" => lex_string_cpt n s' (* \t *)
+      | "010" => lex_string_cpt n s' (* \n *)
+      | "013" => lex_string_cpt n s' (* \r *)
+      | "(" => option_map (Buf_cons (LPAREN tt)) (lex_string_cpt n s')
+      | ")" => option_map (Buf_cons (RPAREN tt)) (lex_string_cpt n s')
+      | "+" => option_map (Buf_cons (ADD tt)) (lex_string_cpt n s')
+      | "-" => option_map (Buf_cons (SUB tt)) (lex_string_cpt n s')
+      | "*" => option_map (Buf_cons (MUL tt)) (lex_string_cpt n s')
+      | "/" => option_map (Buf_cons (DIV tt)) (lex_string_cpt n s')
+      | _ =>
+        if is_digit c then
+          let (m,s) := readnum 0 s in
+          option_map (Buf_cons (NUM m)) (lex_string_cpt n s)
+        else if is_alpha c then
+          let k := identsize s in
+          let id := substring 0 k s in
+          let s := ntail k s in
+          option_map (Buf_cons (ID id)) (lex_string_cpt n s)
+        else None
+      end
+    end
+  end.
+
+Definition lex_string s := lex_string_cpt (length s) s.

demos/coq-minicalc/Makefile

+MENHIR            := menhir
+MENHIRFLAGS       := --coq
+COQINCLUDES       :=
+
+Makefile.coq:
+	coq_makefile -o Makefile.coq Lexer.v MiniCalc.v Parser.v $(COQINCLUDES)
+
+Parser.v : Parser.vy
+	$(MENHIR) $(MENHIRFLAGS) $<
+
+include Makefile.coq
+
+clean::
+	rm -f Parser.v
+	rm -f Makefile.coq Makefile.coq.conf
+	rm -f .*.aux

demos/coq-minicalc/MiniCalc.v

+
+Require Import Parser Lexer List String PeanoNat.
+Import MenhirLibParser.Inter.
+Import ListNotations.
+Open Scope string_scope.
+
+(** Lexer + Parser for little arithmetic expressions *)
+
+Definition string2expr s :=
+  match option_map (Parser.parse_expr 50) (Lexer.lex_string s) with
+  | Some (Parsed_pr f _) => Some f
+  | _ => None
+  end.
+
+(** Let's print back our little expressions *)
+
+Module Print.
+
+Definition pr_digit n :=
+  match n with
+  | 0 => "0"
+  | 1 => "1"
+  | 2 => "2"
+  | 3 => "3"
+  | 4 => "4"
+  | 5 => "5"
+  | 6 => "6"
+  | 7 => "7"
+  | 8 => "8"
+  | _ => "9"
+  end.
+
+Fixpoint prnat_loop n k :=
+  match k with
+  | 0 => ""
+  | S k =>
+    match n/10 with
+    | 0 => pr_digit n
+    | q => prnat_loop q k ++ pr_digit (n mod 10)
+    end
+  end.
+
+Definition prnat n := prnat_loop n (S n).
+
+Fixpoint pr_expr e :=
+ match e with
+ | Ast.Num n => prnat n
+ | Ast.Var x => x
+ | Ast.Add e e' => "(" ++ pr_expr e ++ "+" ++ pr_expr e' ++ ")"
+ | Ast.Sub e e' => "(" ++ pr_expr e ++ "-" ++ pr_expr e' ++ ")"
+ | Ast.Mul e e' => "(" ++ pr_expr e ++ "*" ++ pr_expr e' ++ ")"
+ | Ast.Div e e' => "(" ++ pr_expr e ++ "/" ++ pr_expr e' ++ ")"
+ end.
+
+End Print.
+
+Definition example := "12 + 34*x / (48+y)".
+Definition expected_reprint := "(12+((34*x)/(48+y)))".
+
+Compute option_map Print.pr_expr (string2expr example).
+
+Definition check :=
+  match option_map Print.pr_expr (string2expr example) with
+  | Some s => if string_dec s expected_reprint then "OK" else "KO"
+  | None => "KO"
+  end.
+
+(** This should display "OK" *)
+
+Compute check.

demos/coq-minicalc/Parser.vy

+(* Grammar for little arithmetic expressions (+-*/) *)
+
+%{
+
+Require Import String.
+
+Module Ast.
+Inductive expr :=
+ | Var : string -> expr
+ | Num : nat -> expr
+ | Add : expr -> expr -> expr
+ | Sub : expr -> expr -> expr
+ | Mul : expr -> expr -> expr
+ | Div : expr -> expr -> expr.
+End Ast.
+
+%}
+
+%token ADD SUB MUL DIV LPAREN RPAREN EOF
+%token<nat> NUM
+%token<string> ID
+
+%start<Ast.expr> parse_expr
+%type<Ast.expr> p_expr
+%type<Ast.expr> p_factor
+%type<Ast.expr> p_atom
+
+%%
+
+parse_expr : p_expr EOF       { $1 }
+
+p_atom :
+  ID                          { Ast.Var $1 }
+| NUM                         { Ast.Num $1 }
+| LPAREN p_expr RPAREN        { $2 } 
+
+p_expr :
+| p_factor                    { $1 }
+| p_expr ADD p_factor         { Ast.Add $1 $3 }
+| p_expr SUB p_factor         { Ast.Sub $1 $3 }
+
+p_factor :
+| p_atom                      { $1 }
+| p_factor MUL p_atom         { Ast.Mul $1 $3 }
+| p_factor DIV p_atom         { Ast.Div $1 $3 }

demos/coq-minicalc/README.md

+
+Coq-MiniCalc : a little demo of Lexing/Parsing in Coq
+=====================================================
+
+Pierre Letouzey, 2019
+
+Licence : CC0
+
+This is a toy demo of the recent Coq backend of `menhir`.
+
+This micro-grammar recognizes arithmetic expressions : numbers, idents, `+` `*` `-` `/` and parenthesis.
+We provide an hand-written lexer, and a minimal final test (compilation should display "OK").
+
+Tested with Coq 8.8 + menhir 2019/06/13 + corresponding coq-menhirlib.
+Anything more recent than that should be ok.
\ No newline at end of file

demos/coq-minicalc/_CoqProject

+-I .
+-R . MiniCalc
+
+Parser.v
+Lexer.v
+MiniCalc.v

doc/manual.html

@@ -58,13 +58,13 @@ font-size: 1rem;
 }
 </style>
 <title>Menhir Reference Manual 
-(version 20190626)
+(version 20190924)
 </title>
 </head>
 <body >
 <!--HEVEA command line is: hevea -fix manual.tex -->
 <!--CUT STYLE article--><!--CUT DEF section 1 --><table class="title"><tr><td style="padding:1ex"><h1 class="titlemain">Menhir Reference Manual<br>
-(version 20190626)</h1><h3 class="titlerest">François Pottier and Yann Régis-Gianas<br>
+(version 20190924)</h1><h3 class="titlerest">François Pottier and Yann Régis-Gianas<br>
 INRIA<br>
 <span style="font-family:monospace">{Francois.Pottier, Yann.Regis-Gianas}@inria.fr</span></h3></td></tr>
 </table><!--TOC section id="sec1" Contents-->
@@ -281,10 +281,8 @@ which is printed on the standard output channel.</p><p><span style="font-family:
 the grammar specification to be translated into a definition of the <span style="font-family:monospace">token</span> type, which is written to the files <span style="font-style:italic">basename</span><span style="font-family:monospace">.ml</span> and
 <span style="font-style:italic">basename</span><span style="font-family:monospace">.mli</span>. No code is generated. This is useful when
 a single set of tokens is to be shared between several parsers. The directory
-<a href="https://gitlab.inria.fr/fpottier/menhir/blob/master/demos/calc-two"><span style="font-family:monospace">demos/calc-two</span></a> contains a demo that illustrates the use of this switch.</p><p><span style="font-family:monospace">--raw-depend</span>.  See §<a href="#sec%3Abuild">14</a>.</p><p><span style="font-family:monospace">--stdlib</span> <span style="font-style:italic">directory</span>.  This switch controls the directory where
-the standard library (§<a href="#sec%3Alibrary">5.4</a>) is found. It takes precedence over
-both the installation-time directory and the directory that may be specified
-via the environment variable <code>$MENHIR_STDLIB</code>.</p><p><span style="font-family:monospace">--strict</span>.  This switch causes several warnings about the grammar
+<a href="https://gitlab.inria.fr/fpottier/menhir/blob/master/demos/calc-two"><span style="font-family:monospace">demos/calc-two</span></a> contains a demo that illustrates the use of this switch.</p><p><span style="font-family:monospace">--raw-depend</span>.  See §<a href="#sec%3Abuild">14</a>.</p><p><span style="font-family:monospace">--stdlib</span> <span style="font-style:italic">directory</span>.  This switch exists only for
+backwards compatibility and is ignored. It may be removed in the future.</p><p><span style="font-family:monospace">--strict</span>.  This switch causes several warnings about the grammar
 and about the automaton to be considered errors. This includes warnings about
 useless precedence declarations, non-terminal symbols that produce the empty
 language, unreachable non-terminal symbols, productions that are never
@@ -1130,13 +1128,7 @@ more elaborate notions. For instance, the following rule:
 causes <span style="font-style:italic">plist</span>(<span style="font-style:italic">X</span>) to recognize a list of <span style="font-style:italic">X</span>’s, where the empty
 list is represented by the empty string, and a non-empty list is delimited
 with parentheses and comma-separated.</p><p>The standard library is stored in a file named <a href="https://gitlab.inria.fr/fpottier/menhir/blob/master/src/standard.mly"><span style="font-family:monospace">standard.mly</span></a>, which is
-installed at the same time as Menhir. By default, Menhir attempts to find this
-file in the directory where this file was installed. This can be overridden by
-setting the environment variable
-<code>$MENHIR_STDLIB</code>. If defined, this variable should contain the path of
-the directory where <span style="font-family:monospace">standard.mly</span> is stored. (This path may
-end with a <span style="font-family:monospace">/</span> character.) This can be overridden also via the
-command line switch <span style="font-family:monospace">--stdlib</span>.
+embedded inside Menhir when it is built.
 The command line switch <span style="font-family:monospace">--no-stdlib</span> instructs Menhir to <em>not</em> load the
 standard library.</p><p>The meaning of the symbols defined in the standard library
 (Figure <a href="#fig%3Astandard">3</a>) should be clear in most cases. Yet, the