diff --git a/MenhirLib/Interpreter.v b/MenhirLib/Interpreter.v index c125ca548..aa0e823db 100644 --- a/MenhirLib/Interpreter.v +++ b/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. diff --git a/configure b/configure index 3ed6b870e..84e4007b5 100755 --- a/configure +++ b/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." diff --git a/coq-compcert-32.opam b/coq-compcert-32.opam new file mode 100644 index 000000000..623bab9ef --- /dev/null +++ b/coq-compcert-32.opam @@ -0,0 +1,57 @@ +opam-version: "2.0" +authors: "Xavier Leroy " +maintainer: "Jacques-Henri Jourdan " +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" +]