Support development Menhir and Rocq 9.3 proof syntax

MenhirLib/Interpreter.v

@@ -174,6 +174,7 @@ Fixpoint pop (symbols_to_pop:list symbol) {A:Type} (stk:stack) :
   thunkP (prefix symbols_to_pop (symb_stack_of_stack stk)) ->
   forall (action:arrows_right A (map symbol_semantic_type symbols_to_pop)),
     stack * A.
+Proof.
 unshelve refine
   (match symbols_to_pop
       return
@@ -191,7 +192,6 @@ unshelve refine
          | [] => fun Hp => False_rect _ _
        end Hp
    end).
-Proof.
   - simpl in Hp. clear -Hp. abstract (intros _ ; specialize (Hp I); now inversion Hp).
   - clear -Hp. abstract (specialize (Hp I); now inversion Hp).
   - simpl in Hp. clear -Hp. abstract (intros _ ; specialize (Hp I); now inversion Hp).
@@ -288,6 +288,7 @@ Definition reduce_step stk prod (buffer : buffer)
         (Hval : thunkP (valid_for_reduce (state_of_stack stk) prod))
         (Hi : thunkP (stack_invariant stk))
   : step_result.
+Proof.
 refine
   ((let '(stk', sem) as ss := pop (prod_rhs_rev prod) stk _ (prod_action prod)
       return thunkP (state_valid_after_pop (state_of_stack (fst ss)) _
@@ -308,7 +309,6 @@ refine
       Accept_sr sem buffer
     end (fun _ => _))
    (fun _ => pop_state_valid _ _ _ _ _ _ _)).
-Proof.
   - clear -Hi Hval.
     abstract (intros _; destruct Hi=>//; eapply prefix_trans; [by apply Hval|eassumption]).
   - clear -Hval.
@@ -434,12 +434,12 @@ Global Arguments parse_result _ : clear implicits.
 
 Definition parse (buffer : buffer) (log_n_steps : nat):
   parse_result (symbol_semantic_type (NT (start_nt init))).
+Proof.
 refine (match proj1_sig (parse_fix [] buffer log_n_steps _) with
         | Fail_sr_full st tok => Fail_pr_full st tok
         | Accept_sr sem buffer' => Parsed_pr sem buffer'
         | Progress_sr _ _ => Timeout_pr
         end).
-Proof.
   abstract (repeat constructor; intros; by destruct singleton_state_pred).
 Defined.
 

configure

@@ -616,7 +616,7 @@ fi
 
 MENHIR_REQUIRED=20200624
 echo "Testing Menhir... " | tr -d '\n'
-menhir_ver=$(menhir --version 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p')
+menhir_ver=$(menhir --version 2>/dev/null | sed -n -E -e 's/^.*version (unreleased|[0-9]*).*$/\1/p')
 case "$menhir_ver" in
   20[0-9][0-9][0-9][0-9][0-9][0-9])
       if test "$menhir_ver" -ge $MENHIR_REQUIRED; then
@@ -636,6 +636,20 @@ case "$menhir_ver" in
           echo "Error: CompCert requires a version greater or equal to $MENHIR_REQUIRED."
           missingtools=true
       fi;;
+  unreleased)
+      # Development ("unreleased") builds of Menhir, e.g. an opam pin on the
+      # upstream git repository.  Assume they are recent enough.
+      echo "version $menhir_ver -- acceptable!"
+      menhir_dir=$(ocamlfind query menhirLib 2>/dev/null) || \
+      menhir_dir=$(menhir --suggest-menhirLib) || \
+      menhir_dir=""
+      menhir_dir=$(echo "$menhir_dir" | tr -d '\r' | tr '\\' '/')
+      if test ! -d "$menhir_dir"; then
+          echo "Error: cannot determine the location of the Menhir API library."
+          echo "This can be due to an incorrect Menhir package."
+          echo "Consider using the OPAM package for Menhir."
+          missingtools=true
+      fi;;
   *)
         echo "NOT FOUND"
         echo "Error: make sure Menhir version $MENHIR_REQUIRED or later is installed."

coq-compcert-32.opam

@@ -0,0 +1,57 @@
+opam-version: "2.0"
+authors: "Xavier Leroy <xavier.leroy@inria.fr>"
+maintainer: "Jacques-Henri Jourdan <jacques-Henri.jourdan@normalesup.org>"
+homepage: "http://compcert.inria.fr/"
+dev-repo: "git+https://github.com/AbsInt/CompCert.git"
+bug-reports: "https://github.com/AbsInt/CompCert/issues"
+license: "INRIA Non-Commercial License Agreement"
+available: os != "macos"
+build: [
+  ["./configure"
+  "ia32-linux" {os = "linux"}
+  "ia32-cygwin" {os = "cygwin"}
+  # This is for building a MinGW CompCert with cygwin host and cygwin target
+  "ia32-cygwin" {os = "win32" & os-distribution = "cygwinports"}
+  # This is for building a 32 bit CompCert on 64 bit MinGW with cygwin build host
+  "-toolprefix"     {os = "win32" & os-distribution = "cygwinports" & arch = "x86_64"}
+  "i686-pc-cygwin-" {os = "win32" & os-distribution = "cygwinports" & arch = "x86_64"}
+  # The 32 bit CompCert is a variant which is installed in a non standard folder
+  "-prefix" "%{prefix}%/variants/compcert32"
+  "-install-coqdev"
+  "-clightgen"
+  "-use-external-Flocq"
+  "-use-external-MenhirLib"
+  "-coqdevdir" "%{lib}%/coq-variant/compcert32/compcert"
+  "-ignore-coq-version"]
+  [make "-j%{jobs}%" {ocaml:version >= "4.06"}]
+]
+install: [
+  [make "install"]
+]
+depends: [
+  "coq" {>= "8.8" | = "dev"}
+  "menhir" {>= "20190626" | = "dev"}
+  "ocaml" {>= "4.05.0"}
+  "coq-flocq" {>= "3.1.0" & < "4.0.0"} | "coq-flocq3" {= "dev"}
+  "coq-menhirlib" {>= "20190626" | = "dev"}
+]
+synopsis: "The CompCert C compiler (32 bit)"
+description: "This package installs the 32 bit version of CompCert.
+For coexistence with the 64 bit version, the files are installed in:
+%{prefix}%/variants/compcert32/bin  (ccomp and clightgen binaries)
+%{prefix}%/variants/compcert32/lib/compcert  (C library)
+%{lib}%/coq-variant/compcert32/compcert (Coq library)
+Please note that the coq module path is compcert and not compcert32,
+so the files cannot be directly Required as compcert32.
+Instead -Q or -R options must be used to bind the compcert32 folder
+to the module path compcert. This is more convenient if one development
+supports both 32 and 64 bit versions. Otherwise all files would have to
+be duplicated with module paths compcert and compcert32.
+Please also note that the binary folder is usually not in the path."
+tags: [
+  "category:Computer Science/Semantics and Compilation/Compilation"
+  "category:Computer Science/Semantics and Compilation/Semantics"
+  "keyword:C"
+  "keyword:compiler"
+  "logpath:compcert32"
+]