Merge pull request #60 from harp-project/feature/upgrade-rocq

Upgrade to Rocq 9.1

Author: berpeti

.github/workflows/docker-action.yml

@@ -19,7 +19,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'coqorg/coq:8.20'
+          - 'rocq/rocq-prover:9.1'
       fail-fast: false
     steps:
       - uses: actions/checkout@v4
@@ -30,6 +30,8 @@ jobs:
           before_install: |
             startGroup "Setup and print opam config"
               opam repo -a --set-default add coq-extra-dev https://coq.inria.fr/opam/extra-dev
+              opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
+              opam install rocq-stdpp
               opam config list; opam repo list; opam list
             endGroup
 

Makefile

@@ -9,7 +9,7 @@ KNOWNFILES   := Makefile _CoqProject
 .DEFAULT_GOAL := invoke-coqmakefile
 
 CoqMakefile: Makefile _CoqProject
-	$(COQBIN)coq_makefile -f _CoqProject -o CoqMakefile
+	$(COQBIN)rocq makefile -f _CoqProject -o CoqMakefile
 
 invoke-coqmakefile: CoqMakefile
 	$(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))

README.md

@@ -12,7 +12,7 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 
 
-In this repository you can find the formalisation of a subset of Core Erlang in Coq Proof Assistant. The main features of the formalisation include:
+In this repository you can find the formalisation of a subset of Core Erlang in Rocq. The main features of the formalisation include:
 - The syntax of Core Erlang
 - A big-step, a functional big-step and a frame stack semantics of sequential Core Erlang
 - A frame stack semantics for a subset of concurrent Core Erlang
@@ -30,7 +30,7 @@ In this repository you can find the formalisation of a subset of Core Erlang in
   - Simon Thompson
   - M.Sc. students from Eötvös Loránd University
 - License: [GNU Lesser General Public License v3 or later](LICENSE)
-- Compatible Rocq/Coq versions: 8.20
+- Compatible Rocq/Coq versions: 9.1
 - Additional dependencies:
   - [Stdpp](https://gitlab.mpi-sws.org/iris/stdpp) 1.11.0 is required
 - Rocq/Coq namespace: `CoreErlang`
@@ -46,13 +46,13 @@ In this repository you can find the formalisation of a subset of Core Erlang in
 
 ## Compiling the project
 
-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.
+Necessary requirements: Rocq v9.1.0, stdpp v1.11.0 and Erlang/OTP v23.0 (not necessary for the Rocq developments). The library is compilable by using `make`. In the following list, we give a brief description about the contents of the files.
 
 ## Structure of the formalisation
 
 The main module `CoreErlang` includes the common features for all semantics:
 
-- `src/Basics.v`: fundamental types, and lemmas about them and the built-in features of Coq;
+- `src/Basics.v`: fundamental types, and lemmas about them and the built-in features of Rocq;
 - `src/Syntax.v`: the abstract syntax of Core Erlang;
 - `src/Induction.v`: induction principles for the syntax;
 - `src/Equalities.v`: decidable and boolean equalities and comparison based on the abstract syntax;
@@ -123,15 +123,15 @@ Concurrent semantics based on the sequential semantics of `FrameStack` is define
 
 ## Formally based interpreter for Core Erlang
 
-The interpreter based on the formal semantics is implemented in `src/Interpreter`, which features function-based variants for the frame stack semantics defined in `src/FrameStack` and `src/Concurrent`. The interpreter is based on Coq's extraction mechanism.
+The interpreter based on the formal semantics is implemented in `src/Interpreter`, which features function-based variants for the frame stack semantics defined in `src/FrameStack` and `src/Concurrent`. The interpreter is based on Rocq's extraction mechanism.
 
 - `src/Interpreter/Equivalences.v`: proves the equivalence of the frame stack semantics and its function-based variants (implemented in `StepFunctions.v`) for both the sequential and concurrent sublanguages.
-- `src/Interpreter/ExampleProgExtraction.v`: includes a Coq script to extract the (parsed Erlang) programs defined in `src/interpreter/ExampleASTs/coqAST`.
-- `src/Interpreter/HaskellExtraction.v`: includes a Coq script to extract the (functional) semantics to Haskell. This script also optimises the semantics in several aspects with extraction commands.
-- `src/Interpreter/HaskellExtractionQuickCheck.v`: includes a Coq script to extract the (functional) semantics to Haskell without optimisations.
+- `src/Interpreter/ExampleProgExtraction.v`: includes a Rocq script to extract the (parsed Erlang) programs defined in `src/interpreter/ExampleASTs/rocqAST`.
+- `src/Interpreter/HaskellExtraction.v`: includes a Rocq script to extract the (functional) semantics to Haskell. This script also optimises the semantics in several aspects with extraction commands.
+- `src/Interpreter/HaskellExtractionQuickCheck.v`: includes a Rocq script to extract the (functional) semantics to Haskell without optimisations.
 - `src/Interpreter/InterpreterAux.v`: defines a number of helper functions for the function-based semantics.
 - `src/Interpreter/InterpreterAuxLemmas.v`: proves a number of properties of the helper functions mentioned above.
-- `src/Interpreter/OCamlExtraction.v`: includes a Coq script to extract the (functional) semantics to OCaml without optimisations.
+- `src/Interpreter/OCamlExtraction.v`: includes a Rocq script to extract the (functional) semantics to OCaml without optimisations.
 - `src/Interpreter/Scheduler.v`: defines a number of helper functions used by the scheduler implemented in Haskell.
 - `src/Interpreter/StepFunctions.v`: defines the function-based variants of the frame stack semantics.
 - `src/Interpreter/Tests.v`: includes a number of unit tests for the function-based semantics.

coq-core-erlang-formalization.opam

@@ -10,9 +10,9 @@ dev-repo: "git+https://github.com/harp-project/core-erlang-formalization.git"
 bug-reports: "https://github.com/harp-project/core-erlang-formalization/issues"
 license: "LGPL-3.0-or-later"
 
-synopsis: "Core Erlang Formalisation in Coq"
+synopsis: "Core Erlang Formalisation in Rocq"
 description: """
-In this repository you can find the formalisation of a subset of Core Erlang in Coq Proof Assistant. The main features of the formalisation include:
+In this repository you can find the formalisation of a subset of Core Erlang in Rocq. The main features of the formalisation include:
 - The syntax of Core Erlang
 - A big-step, a functional big-step and a frame stack semantics of sequential Core Erlang
 - A frame stack semantics for a subset of concurrent Core Erlang
@@ -25,8 +25,8 @@ In this repository you can find the formalisation of a subset of Core Erlang in
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { >= "8.20" }
-  "coq-stdpp" { = "1.11.0"}
+  "coq" { >= "9.1" }
+  "rocq-stdpp" dev
 ]
 
 tags: [

meta.yml

@@ -7,10 +7,10 @@ action: true
 # circleci: true
 coqdoc: false
 
-synopsis: Core Erlang Formalisation in Coq
+synopsis: Core Erlang Formalisation in Rocq
 
 description: |
-    In this repository you can find the formalisation of a subset of Core Erlang in Coq Proof Assistant. The main features of the formalisation include:
+    In this repository you can find the formalisation of a subset of Core Erlang in Rocq. The main features of the formalisation include:
     - The syntax of Core Erlang
     - A big-step, a functional big-step and a frame stack semantics of sequential Core Erlang
     - A frame stack semantics for a subset of concurrent Core Erlang
@@ -55,20 +55,21 @@ license:
   identifier: LGPL-3.0-or-later
 
 supported_coq_versions:
-  text: "8.20"
-  opam: '{ >= "8.20" }'
+  text: "9.1"
+  opam: '{ >= "9.1" }'
 
 opam-file-version: dev
 
-tested_coq_opam_versions:
-#- version: dev
-- version: '8.20'
+tested_rocq_opam_versions:
+- version: '9.1'
 
 ci_extra_dev: true
 dependencies:
 - opam:
-    name: coq-stdpp
-    version: '{ = "1.11.0"}'
+    name: rocq-stdpp
+    version: dev #'{ = "1.11.0"}'
+    # TODO stdpp is not yet released in opam for Rocq 9.1
+    # TODO: Manually added to docker-action.yml -> before-install: opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git & opam install rocq-stdpp
   description: |-
     [Stdpp](https://gitlab.mpi-sws.org/iris/stdpp) 1.11.0 is required
 
@@ -89,14 +90,14 @@ keywords:
 build: |-
     ## Compiling the project
 
-    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.
+    Necessary requirements: Rocq v9.1.0, stdpp v1.11.0 and Erlang/OTP v23.0 (not necessary for the Rocq developments). The library is compilable by using `make`. In the following list, we give a brief description about the contents of the files.
 
 documentation: |-
     ## Structure of the formalisation
 
     The main module `CoreErlang` includes the common features for all semantics:
 
-    - `src/Basics.v`: fundamental types, and lemmas about them and the built-in features of Coq;
+    - `src/Basics.v`: fundamental types, and lemmas about them and the built-in features of Rocq;
     - `src/Syntax.v`: the abstract syntax of Core Erlang;
     - `src/Induction.v`: induction principles for the syntax;
     - `src/Equalities.v`: decidable and boolean equalities and comparison based on the abstract syntax;
@@ -167,15 +168,15 @@ documentation: |-
 
     ## Formally based interpreter for Core Erlang
     
-    The interpreter based on the formal semantics is implemented in `src/Interpreter`, which features function-based variants for the frame stack semantics defined in `src/FrameStack` and `src/Concurrent`. The interpreter is based on Coq's extraction mechanism.
+    The interpreter based on the formal semantics is implemented in `src/Interpreter`, which features function-based variants for the frame stack semantics defined in `src/FrameStack` and `src/Concurrent`. The interpreter is based on Rocq's extraction mechanism.
     
     - `src/Interpreter/Equivalences.v`: proves the equivalence of the frame stack semantics and its function-based variants (implemented in `StepFunctions.v`) for both the sequential and concurrent sublanguages.
-    - `src/Interpreter/ExampleProgExtraction.v`: includes a Coq script to extract the (parsed Erlang) programs defined in `src/interpreter/ExampleASTs/coqAST`.
-    - `src/Interpreter/HaskellExtraction.v`: includes a Coq script to extract the (functional) semantics to Haskell. This script also optimises the semantics in several aspects with extraction commands.
-    - `src/Interpreter/HaskellExtractionQuickCheck.v`: includes a Coq script to extract the (functional) semantics to Haskell without optimisations.
+    - `src/Interpreter/ExampleProgExtraction.v`: includes a Rocq script to extract the (parsed Erlang) programs defined in `src/interpreter/ExampleASTs/rocqAST`.
+    - `src/Interpreter/HaskellExtraction.v`: includes a Rocq script to extract the (functional) semantics to Haskell. This script also optimises the semantics in several aspects with extraction commands.
+    - `src/Interpreter/HaskellExtractionQuickCheck.v`: includes a Rocq script to extract the (functional) semantics to Haskell without optimisations.
     - `src/Interpreter/InterpreterAux.v`: defines a number of helper functions for the function-based semantics.
     - `src/Interpreter/InterpreterAuxLemmas.v`: proves a number of properties of the helper functions mentioned above.
-    - `src/Interpreter/OCamlExtraction.v`: includes a Coq script to extract the (functional) semantics to OCaml without optimisations.
+    - `src/Interpreter/OCamlExtraction.v`: includes a Rocq script to extract the (functional) semantics to OCaml without optimisations.
     - `src/Interpreter/Scheduler.v`: defines a number of helper functions used by the scheduler implemented in Haskell.
     - `src/Interpreter/StepFunctions.v`: defines the function-based variants of the frame stack semantics.
     - `src/Interpreter/Tests.v`: includes a number of unit tests for the function-based semantics.

src/Auxiliaries.v

@@ -16,9 +16,9 @@
 *)
 
 From CoreErlang Require Export SideEffects ScopingLemmas Equalities.
-Require Export Coq.Sorting.Permutation.
-Require Export Ascii.
-Require Export Numbers.DecimalString Decimal.
+Require Export Stdlib.Sorting.Permutation.
+From Stdlib Require Export Ascii.
+From Stdlib Require Export Numbers.DecimalString Decimal.
 
 Import ListNotations.
 
@@ -639,7 +639,7 @@ Proof.
     now apply IHl2.
 Qed.
 
-(** Scope of transforming a Core Erlang list to a Coq list *)
+(** Scope of transforming a Core Erlang list to a Rocq list *)
 Lemma mk_list_closed :
   forall l l' Γ,
     VAL Γ ⊢ l ->
@@ -653,7 +653,7 @@ Proof.
   reflexivity.
 Qed.
 
-(** Scope of transforming a Coq list into a Core Erlang list *)
+(** Scope of transforming a Rocq list into a Core Erlang list *)
 Lemma meta_to_cons_closed :
   forall l Γ,
     Forall (ValScoped Γ) l ->

src/Basics.v

@@ -4,9 +4,9 @@
   transform goals and hypotheses
  *)
 
-Require Export Coq.micromega.Lia
-               Coq.Lists.List
-               Coq.Arith.PeanoNat.
+Require Export Stdlib.micromega.Lia
+               Stdlib.Lists.List
+               Stdlib.Arith.PeanoNat.
 Import ListNotations.
 
 (**

src/BigStep/Auxiliaries.v

@@ -6,7 +6,7 @@
 *)
 
 From CoreErlang.BigStep Require Export SideEffects.
-Require Export Coq.Sorting.Permutation.
+Require Export Stdlib.Sorting.Permutation.
 
 Import ListNotations.
 

src/BigStep/BigStep.v

@@ -7,7 +7,9 @@ From CoreErlang.BigStep Require Export ModuleAuxiliaries.
 (** The Semantics of Core Erlang *)
 Import ListNotations.
 
+Set Warnings "-closed-notation-not-level-0".
 Reserved Notation "| env , modules , own_module , id , e , eff | -e> | id' , e' , eff' |" (at level 70).
+Set Warnings "+closed-notation-not-level-0".
 (* Reserved Notation "| env , id , e , eff | -s> | id' , e' , eff' |" (at level 70). *)
 Inductive eval_expr : Environment -> list ErlModule -> string -> nat -> Expression -> SideEffectList -> nat ->
     (ValueSequence + Exception) -> SideEffectList -> Prop :=

src/BigStep/Coverage.v

@@ -4,7 +4,7 @@
 *)
 
 From CoreErlang.BigStep Require Export ModuleAuxiliaries.
-(* From Coq Require FSets.FMapWeakList. *)
+(* From Stdlib Require FSets.FMapWeakList. *)
 Require Import FunctionalBigStep.
 
 Import ListNotations.