Merge pull request #35 from harp-project/coq-8-20

Upgrade to Coq version 8.20

Makefile

@@ -7,7 +7,7 @@
 ##         #     GNU Lesser General Public License Version 2.1          ##
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
-## GNUMakefile for Coq 8.19.0
+## GNUMakefile for Coq 8.20.0
 
 # For debugging purposes (must stay here, don't move below)
 INITIAL_VARS := $(.VARIABLES)
@@ -278,7 +278,7 @@ COQDOCLIBS?=$(COQLIBS_NOML)
 # The version of Coq being run and the version of coq_makefile that
 # generated this makefile
 COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
-COQMAKEFILE_VERSION:=8.19.0
+COQMAKEFILE_VERSION:=8.20.0
 
 # COQ_SRC_SUBDIRS is for user-overriding, usually to add
 # `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for
@@ -309,7 +309,7 @@ endif
 
 ifneq (,$(PROFILING))
   PROFILE_ARG=-profile $<.prof.json
-  PROFILE_ZIP=gzip $<.prof.json
+  PROFILE_ZIP=gzip -f $<.prof.json
 else
   PROFILE_ARG=
   PROFILE_ZIP=true
@@ -503,37 +503,6 @@ bytefiles: $(CMOFILES) $(CMAFILES)
 optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES))
 .PHONY: optfiles
 
-# FIXME, see Ralf's bugreport
-# quick is deprecated, now renamed vio
-vio: $(VOFILES:.vo=.vio)
-.PHONY: vio
-quick: vio
-	$(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files")
-.PHONY: quick
-
-vio2vo:
-	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
-		-schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
-.PHONY: vio2vo
-
-# quick2vo is undocumented
-quick2vo:
-	$(HIDE)make -j $(J) vio
-	$(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \
-	  viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \
-	  if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \
-	done); \
-	echo "VIO2VO: $$VIOFILES"; \
-	if [ -n "$$VIOFILES" ]; then \
-	  $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \
-	fi
-.PHONY: quick2vo
-
-checkproofs:
-	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
-		-schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
-.PHONY: checkproofs
-
 vos: $(VOFILES:%.vo=%.vos)
 .PHONY: vos
 
@@ -711,9 +680,10 @@ clean::
 	$(HIDE)rm -f $(NATIVEFILES)
 	$(HIDE)find . -name .coq-native -type d -empty -delete
 	$(HIDE)rm -f $(VOFILES)
-	$(HIDE)rm -f $(VOFILES:.vo=.vio)
 	$(HIDE)rm -f $(VOFILES:.vo=.vos)
 	$(HIDE)rm -f $(VOFILES:.vo=.vok)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.prof.json)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.prof.json.gz)
 	$(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old)
 	$(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex
 	$(HIDE)rm -f $(VFILES:.v=.glob)
@@ -846,10 +816,6 @@ endif
 
 $(foreach vfile,$(VFILES:.v=),$(eval $(call globvorule,$(vfile))))
 
-$(VFILES:.v=.vio): %.vio: %.v
-	$(SHOW)COQC -vio $<
-	$(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
-
 $(VFILES:.v=.vos): %.vos: %.v
 	$(SHOW)COQC -vos $<
 	$(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<

Makefile.conf

@@ -42,14 +42,14 @@ COQMF_CMDLINE_COQLIBS =
 #                                                                             #
 ###############################################################################
 
-COQMF_COQLIB=/home/berpeti/.opam/default/lib/coq/
-COQMF_COQCORELIB=/home/berpeti/.opam/default/lib/coq/../coq-core/
-COQMF_DOCDIR=/home/berpeti/.opam/default/share/doc/
-COQMF_OCAMLFIND=/home/berpeti/.opam/default/bin/ocamlfind
+COQMF_COQLIB=/home/berpeti/.opam/5.1.1/lib/coq/
+COQMF_COQCORELIB=/home/berpeti/.opam/5.1.1/lib/coq/../coq-core/
+COQMF_DOCDIR=/home/berpeti/.opam/5.1.1/share/doc/
+COQMF_OCAMLFIND=/home/berpeti/.opam/5.1.1/bin/ocamlfind
 COQMF_CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70
 COQMF_WARN=-warn-error +a-3
 COQMF_HASNATDYNLINK=true
-COQMF_COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax
+COQMF_COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/ltac2_ltac1 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax
 COQMF_COQ_NATIVE_COMPILER_DEFAULT=no
 COQMF_WINDRIVE=
 

README.md

@@ -4,7 +4,7 @@ In this repository you can find the formalisation of a sequential subset of Core
 
 # Compilation process
 
-Necessary requirements: Coq v8.19.0, stdpp v1.11.0 and Erlang/OTP v23.0 (not necessary for the Coq developments). The library is compilable by using `make`. In the following list, we give a brief description about the contents of the files.
+Necessary requirements: Coq v8.20.0, stdpp v1.11.0 and Erlang/OTP v23.0 (not necessary for the Coq developments). The library is compilable by using `make`. In the following list, we give a brief description about the contents of the files.
 
 The main module `CoreErlang` includes the common features for all semantics:
 

src/Basics.v

@@ -128,7 +128,7 @@ Section lists.
   Proof.
     intros. destruct (i <? length l1) eqn:P.
     * apply Nat.ltb_lt in P. left. split; [ apply app_nth1 | ]; auto.
-    * apply Nat.ltb_nlt in P. right. split; [ apply app_nth2 | rewrite app_length in H ]; lia.
+    * apply Nat.ltb_nlt in P. right. split; [ apply app_nth2 | rewrite length_app in H ]; lia.
   Qed.
 
   (**
@@ -189,7 +189,7 @@ Section lists.
     forall (l2 l1 : list T) t, l1 = l2 ++ t :: l1 -> False.
   Proof.
     intros. assert (length l1 = length (l2 ++ t :: l1)). { rewrite H at 1. auto. }
-    rewrite app_length in H0. simpl in H0. lia.
+    rewrite length_app in H0. simpl in H0. lia.
   Qed.
 
   (**
@@ -696,8 +696,8 @@ end.
 
 
 (** stdpp's notation for projections *)
-Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1").
-Notation "p .2" := (snd p) (at level 2, left associativity, format "p .2").
+Notation "p .1" := (fst p) (at level 1, left associativity, format "p .1").
+Notation "p .2" := (snd p) (at level 1, left associativity, format "p .2").
 
 (**
   This function replaces the `i`th element of a list, if it exists.

src/Concurrent/BarbedBisim.v

@@ -315,7 +315,7 @@ Proof.
     exists B'', (l' ++ l''). split. 2: split.
     - eapply closureNodeSem_trans; eassumption.
     - assumption.
-    - rewrite app_length. slia.
+    - rewrite length_app. slia.
 Defined.
 
 Lemma barbedExpansion_many_sym :
@@ -336,7 +336,7 @@ Proof.
     exists B'', (l' ++ l''). split. 2: split.
     - eapply closureNodeSem_trans; eassumption.
     - assumption.
-    - rewrite app_length. slia.
+    - rewrite length_app. slia.
 Defined.
 
 Lemma barbedExpansion_trans :

src/Concurrent/BisimRenaming.v

@@ -671,7 +671,7 @@ Proof.
             {
               setoid_rewrite P. simpl.
               eapply forall_biforall with (d1 := SUnlink) (d2 := SUnlink).
-              1: by rewrite map_length.
+              1: by rewrite length_map.
               intros. rewrite map_nth with (d:= SUnlink).
               by apply Signal_eq_renamePID.
             }
@@ -774,7 +774,7 @@ Proof.
           {
             setoid_rewrite P. simpl.
             eapply forall_biforall with (d1 := SUnlink) (d2 := SUnlink).
-            1: by rewrite map_length.
+            1: by rewrite length_map.
             intros. rewrite map_nth with (d:= SUnlink).
             pose proof (Signal_eq_renamePID (nth i l0 SUnlink) p p0).
             unfold Signal_eq in *.
@@ -799,7 +799,7 @@ Proof.
           {
             setoid_rewrite P. simpl.
             eapply forall_biforall with (d1 := SUnlink) (d2 := SUnlink).
-            1: by rewrite map_length.
+            1: by rewrite length_map.
             intros. rewrite map_nth with (d:= SUnlink).
             pose proof (Signal_eq_renamePID (nth i l0 SUnlink) p p0).
             unfold Signal_eq in *.
@@ -824,7 +824,7 @@ Proof.
           {
             setoid_rewrite P. simpl.
             eapply forall_biforall with (d1 := SUnlink) (d2 := SUnlink).
-            1: by rewrite map_length.
+            1: by rewrite length_map.
             intros. rewrite map_nth with (d:= SUnlink).
             pose proof (Signal_eq_renamePID (nth i l0 SUnlink) p p0).
             unfold Signal_eq in *.

src/Concurrent/NodeSemanticsLemmas.v

@@ -531,7 +531,7 @@ Proof.
   * destruct H0_1. subst.
     destruct x. simpl in H4. inv H4.
     put (length : list Signal -> nat) on H4 as Hlen.
-    simpl in Hlen. repeat rewrite app_length in Hlen. simpl in Hlen. lia.
+    simpl in Hlen. repeat rewrite length_app in Hlen. simpl in Hlen. lia.
 Qed.
 
 Lemma no_spawn_included :
@@ -588,7 +588,7 @@ Proof.
     destruct Hlen' as [l' [x ?]]; subst.
     rename n' into n''.
     apply closureNodeSem_trans_rev in H0 as [n' [D1 D2]].
-    rewrite app_length in Hlen. simpl in Hlen. inv D2. inv H6. inv H4.
+    rewrite length_app in Hlen. simpl in Hlen. inv D2. inv H6. inv H4.
     - eapply H with (ι := ι) in D1. 2: lia.
       2: {
         simpl in *; destruct (decide (ι0 = ι)); subst; [
@@ -704,7 +704,7 @@ Proof.
   * pose proof Hl.
     eapply eq_sym, last_element_exists in Hl as [l' [x Eq]]. subst.
     apply closureNodeSem_trans_rev in H0 as [n0' [D1 D2]].
-    rewrite app_length in H2. simpl in *.
+    rewrite length_app in H2. simpl in *.
     inv D2. inv H7.
     eapply H in D1; eauto. lia. inv H5; simpl.
     1-3: repeat processpool_destruct; try congruence.
@@ -1033,7 +1033,7 @@ Proof.
   * pose proof Hl.
     eapply eq_sym, last_element_exists in Hl as [l' [x Eq]]. subst.
     apply closureNodeSem_trans_rev in H0 as [n0' [D1 D2]].
-    rewrite app_length in H2. simpl in *.
+    rewrite length_app in H2. simpl in *.
     inv D2. inv H7. eapply compatibility_of_reduction_rev in H5.
     2: eassumption.
     destruct H5. 2: destruct H0.
@@ -2156,7 +2156,7 @@ Proof.
         apply appearsEther_rename_neq in X; auto.
       }
     - cbn. destruct v1; try now inv H13.
-      case_match; inv H13; simpl; rewrite map_length, H.
+      case_match; inv H13; simpl; rewrite length_map, H.
       2: reflexivity.
       do 2 f_equal. rewrite split_renamePID_subst_exp.
       assert (list_subst