coq-menhirlib/CHANGES.md

 # Changes
 
+## 2019/06/26
+
+* Fix compatibility with Coq 8.7 and Coq 8.9:
+    - In Coq 8.7, in the syntax { x : T & T' } for the sigT types,
+      it was not possible to omit the type T.
+    - An anomaly in Coq 8.7 has been worked around.
+    - In Coq 8.9, the numeral notation for positives moved from
+      Coq.Numbers.BinNums to Coq.PArith.BinPos.
+
 ## 2019/06/13
 
 * The Coq development is now free of any axiom (it used to use axiom

coq-menhirlib/src/Interpreter_complete.v

@@ -353,7 +353,9 @@ Fixpoint build_pt_dot_from_pt {symb word}
       let X :=
           match ptz in pt_zipper symb word
             return match symb with T term => True | NT _ => False end ->
-                   { symbsq & { wordq & (parse_tree_list symbsq wordq *
+                   { symbsq : list symbol &
+                     { wordq : list token &
+                       (parse_tree_list symbsq wordq *
                         ptl_zipper (symb :: symbsq) (wordq ++ word))%type } }
           with
           | Top_ptz => fun F => False_rect _ F

coq-menhirlib/src/Makefile

@@ -18,8 +18,14 @@ clean:
 	@ $(MAKE) -f Makefile.coq --no-print-directory clean
 	@ rm -f _CoqProject
 
+# The role of DESTDIR is explained here:
+# https://www.gnu.org/prep/standards/html_node/DESTDIR.html
+# Basically, it is empty in a normal installation.
+# A nonempty value can be used to perform a dummy installation
+# in a different location.
+
 CONTRIB := $(shell $(COQBIN)coqc -where)/user-contrib
-TARGET  := $(CONTRIB)/MenhirLib
+TARGET  := $(DESTDIR)$(CONTRIB)/MenhirLib
 
 install: all
 	rm -rf $(TARGET)

coq-menhirlib/src/Validator_complete.v

@@ -229,7 +229,7 @@ Proof.
     revert Val. generalize true at 1.
     induction Hfind as [[? ?] l [?%compare_eq ?]|??? IH]=>?.
     + simpl in *; subst.
-      match goal with |- _ -> ?X = true => destruct X end=>//.
+      match goal with |- _ -> ?X = true => destruct X end; [done|].
       rewrite Bool.andb_false_r. clear. induction l as [|[[[??]?]?] l IH]=>//.
     + apply IH.
   - destruct future_of_prod eqn:EQ. by eapply Hval1; eauto.

coq-menhirlib/src/Version.v

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

debian/changelog

-menhir (20190620-1) experimental; urgency=medium
+menhir (20190626-1) experimental; urgency=medium
 
   * New upstream release
+  * Standards-Version 4.3.0 (no change)
   * Build-depend on debhelper-compat(=12); drop file debian/compat
+  * Package libmenhir-ocaml-dev: Suggests ocaml-findlib
   * Override dh_dwz to use --no-dwz-multifile
-  * New binary package: libmenhir-coq.
-  * Standards-Version 4.3.0 (no change)
+  * New binary package: libmenhir-coq
+  * As-installed tests:
+    - Add test for libmenhir-coq (thanks a lot to Pierre Letouzey)
+    - Rename test "calc" to "standalone", tighten test dependencies
 
- -- Ralf Treinen <treinen@debian.org>  Tue, 02 Jul 2019 21:02:40 +0200
+ -- Ralf Treinen <treinen@debian.org>  Wed, 03 Jul 2019 17:59:40 +0200
 
 menhir (20181113-1) unstable; urgency=medium
 

debian/control

@@ -44,6 +44,8 @@ Depends:
   ${misc:Depends}
 Provides:
   ${ocaml:Provides}
+Suggests:
+  ocaml-findlib
 Description: Menhir library 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

debian/copyright

@@ -34,6 +34,10 @@ Files: coq-menhirlib/*
 Copyright: 2018-2019, Inria
 License: LGPL-3+
 
+Files: debian/tests/calcdemo-coq/*
+Copyright: 2019 Pierre Letouzey
+License: CC0
+
 License: GPL-2
  This program is free software; you can redistribute it and/or modify
  it under the terms of the GNU General Public License as published by
@@ -69,3 +73,10 @@ License: LGPL-3+
  On a debian system, the complete license can be found in the file
  /usr/share/common-licenses/GPL-3.
 
+License: CC0
+ These files are distributed under the terms of the Creative Commons
+ license CC0, version 1.0.
+ .
+ On a debian system, the complete license can be found in the file
+ /usr/share/common-licenses/CC0-1.0.
+ 
\ No newline at end of file

debian/patches/coqlib-install

-Author: Ralf Treinen <treinen@debian.org>
-Description: coq-menhirlib: installation must honour $(DESTDIR)
-
-Index: menhir/coq-menhirlib/src/Makefile
-===================================================================
---- menhir.orig/coq-menhirlib/src/Makefile	2019-06-21 21:41:47.909043788 +0200
-+++ menhir/coq-menhirlib/src/Makefile	2019-06-21 21:42:52.321372367 +0200
-@@ -19,7 +19,7 @@
- 	@ rm -f _CoqProject
- 
- CONTRIB := $(shell $(COQBIN)coqc -where)/user-contrib
--TARGET  := $(CONTRIB)/MenhirLib
-+TARGET  := $(DESTDIR)/$(CONTRIB)/MenhirLib
- 
- install: all
- 	rm -rf $(TARGET)

debian/patches/series

-coqlib-install

debian/rules

@@ -42,4 +42,3 @@ override_dh_missing:
 	dh_missing --fail-missing
 
 override_dh_auto_test:
-

debian/tests/calcdemo-coq/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.

debian/tests/calcdemo-coq/Makefile.conf

+# This configuration file was generated by running:
+# coq_makefile -f _CoqProject -o Makefile
+
+
+###############################################################################
+#                                                                             #
+# Project files.                                                              #
+#                                                                             #
+###############################################################################
+
+COQMF_VFILES = Parser.v Lexer.v MiniCalc.v
+COQMF_MLIFILES = 
+COQMF_MLFILES = 
+COQMF_ML4FILES = 
+COQMF_MLPACKFILES = 
+COQMF_MLLIBFILES = 
+COQMF_CMDLINE_VFILES = 
+
+###############################################################################
+#                                                                             #
+# Path directives (-I, -R, -Q).                                               #
+#                                                                             #
+###############################################################################
+
+COQMF_OCAMLLIBS = -I .
+COQMF_SRC_SUBDIRS = .
+COQMF_COQLIBS = -I .  -R . MiniCalc
+COQMF_COQLIBS_NOML =  -R . MiniCalc
+COQMF_CMDLINE_COQLIBS =   
+
+###############################################################################
+#                                                                             #
+# Coq configuration.                                                          #
+#                                                                             #
+###############################################################################
+
+COQMF_LOCAL=1
+COQMF_COQLIB=/home/letouzey/V8//
+COQMF_DOCDIR=/home/letouzey/V8/doc/
+COQMF_OCAMLFIND=/usr/bin/ocamlfind
+COQMF_CAMLP5O=/usr/bin/camlp5o
+COQMF_CAMLP5BIN=/usr/bin/
+COQMF_CAMLP5LIB=/usr/lib/ocaml/camlp5
+COQMF_CAMLP5OPTIONS=-loc loc
+COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-50-58-59   -safe-string
+COQMF_HASNATDYNLINK=true
+COQMF_COQ_SRC_SUBDIRS=config dev lib clib kernel library engine pretyping interp parsing proofs tactics toplevel printing intf grammar ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/fourier plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/quote plugins/romega plugins/rtauto plugins/setoid_ring plugins/ssr plugins/ssrmatching plugins/syntax plugins/xml
+COQMF_WINDRIVE=
+
+###############################################################################
+#                                                                             #
+# Extra variables.                                                            #
+#                                                                             #
+###############################################################################
+
+COQMF_OTHERFLAGS = 
+COQMF_INSTALLCOQDOCROOT = MiniCalc

debian/tests/calcdemo-coq/Makefile.local

+
+Parser.v : Parser.vy
+	menhir --coq $<
+
+clean::
+	rm Parser.v

debian/tests/calcdemo-coq/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.

debian/tests/calcdemo-coq/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 }

debian/tests/calcdemo-coq/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

debian/tests/calcdemo-coq/_CoqProject

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