Bump extraction dependencies (#269)

Author: 4ever2

.github/coq-concert.opam.locked

@@ -19,21 +19,17 @@ depends: [
   "coq-metacoq-template" {= "1.3.4+8.20"}
   "coq-metacoq-template-pcuic" {= "1.3.4+8.20"}
   "coq-metacoq-utils" {= "1.3.4+8.20"}
-  "coq-rust-extraction" {= "dev"}
-  "coq-elm-extraction" {= "0.1.0"}
+  "coq-rust-extraction" {= "0.1.1"}
+  "coq-elm-extraction" {= "0.1.1"}
   "coq-quickchick" {= "2.0.4"}
   "coq-stdpp" {= "1.11.0"}
 ]
-pin-depends: [
-  ["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#c5d9cbae417213fe25b42f08678f28507cc6b99e"]
-]
 build: [
   [make "core"]
   [make "examples"] {with-test}
   [make "html"] {with-doc}
 ]
 install: [
   [make "install"]
-  [make "-C" "examples" "install"] {with-test}
 ]
 dev-repo: "git+https://github.com/AU-COBRA/ConCert.git"

.github/workflows/nix-action-8.20.yml

@@ -13,8 +13,8 @@
     coqPackages.metacoq.override.version = "1.3.4-8.20";
     coqPackages.stdpp.override.version = "1.11.0";
     coqPackages.QuickChick.override.version = "2.0.4";
-    coqPackages.RustExtraction.override.version = "c5d9cbae417213fe25b42f08678f28507cc6b99e";
-    coqPackages.ElmExtraction.override.version = "0.1.0";
+    coqPackages.RustExtraction.override.version = "0.1.1";
+    coqPackages.ElmExtraction.override.version = "0.1.1";
   };
 
   cachix.coq = {};

.nix/config.nix

@@ -1 +1 @@
-"a1f630a232a3e2c739df99d0a947bf7465d2f8bb"
+"944779fa54c48b734298bf78bd71a22eee0abe96"

.nix/coq-nix-toolbox.nix

@@ -24,21 +24,16 @@ depends: [
   "coq-metacoq-pcuic" {>= "1.3.4" & < "1.4~"}
   "coq-metacoq-safechecker" {>= "1.3.4" & < "1.4~"}
   "coq-metacoq-erasure" {>= "1.3.4" & < "1.4~"}
-  "coq-rust-extraction" {= "dev"}
-  "coq-elm-extraction" {= "0.1.0"}
+  "coq-rust-extraction" {= "0.1.1"}
+  "coq-elm-extraction" {= "0.1.1"}
   "coq-stdpp" {>= "1.10.0" & < "1.12~"}
 ]
 
-pin-depends: [
-  ["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#c5d9cbae417213fe25b42f08678f28507cc6b99e"]
-]
-
 build: [
   [make "core"]
   [make "examples"] {with-test}
   [make "html"] {with-doc}
 ]
 install: [
   [make "install"]
-  [make "-C" "examples" "install"] {with-test}
 ]

coq-concert.opam

@@ -15,11 +15,9 @@ From ConCert.Execution Require OptionMonad.
 From ConCert.Execution.Test Require Import LocalBlockchain.
 From ConCert.Examples.BoardroomVoting Require Import BoardroomVotingZ.
 From Coq Require Import List.
-From Coq Require Import String.
 From Coq Require Import ZArith.
 
 
-Local Open Scope string_scope.
 Open Scope Z.
 
 #[local]
@@ -47,7 +45,7 @@ End Params.
 Module BV := BoardroomVoting Params. Import BV.
 
 (* Get string representation of modulus, and remap it. This way we avoid having the extraction compute the number. *)
-Definition modulus_ := StringExtra.string_of_Z modulus.
+Definition modulus_ := BytestringExtra.string_of_Z modulus.
 
 Definition setupWchain := (BV.Setup × Chain).
 
@@ -147,7 +145,7 @@ Definition BV_MODULE : CameLIGOMod BV.Msg ContractCallContext (Address * Setup)
     lmd_module_name := "cameligo_boardroomvoting" ;
 
     (* definitions of operations on pairs and ints *)
-    lmd_prelude := concat nl [CameLIGOPretty.CameLIGOPrelude; extra_ops; hash_func_def];
+    lmd_prelude := String.concat nl [CameLIGOPretty.CameLIGOPrelude; extra_ops; hash_func_def];
 
     (* initial storage *)
     lmd_init := init;
@@ -160,7 +158,7 @@ Definition BV_MODULE : CameLIGOMod BV.Msg ContractCallContext (Address * Setup)
     lmd_receive := receive_wrapper;
 
     (* code for the entry point *)
-    lmd_entry_point := CameLIGOPretty.printMain (PREFIX ++ "receive_wrapper")
+    lmd_entry_point := CameLIGOPretty.printMain (PREFIX ++ "receive_wrapper")%bs
                         "msg"
                         "state"
   |}.
@@ -302,7 +300,7 @@ Definition TT_rename : list (string * string) :=
   ; ("true", "true")
   ; ("false", "false")
   ; ("hash", "hash_")
-  ; (String.to_string (string_of_kername <%% BV.State %%>), "state") (* we add [storage] so it is printed without the prefix *)
+  ; ((string_of_kername <%% BV.State %%>), "state") (* we add [storage] so it is printed without the prefix *)
   ; ("tt", "()")
   ].
 
@@ -311,4 +309,4 @@ Time MetaCoq Run (CameLIGO_prepare_extraction to_inline TT_remap TT_rename [] "c
 Time Definition cameLIGO_boardroomvoting := Eval vm_compute in cameligo_boardroomvoting_prepared.
 
 Redirect "cameligo-extract/BoardroomVoting.mligo"
-MetaCoq Run (tmMsg (String.of_string cameLIGO_boardroomvoting)).
+MetaCoq Run (tmMsg cameLIGO_boardroomvoting).

examples/boardroomVoting/BoardroomVotingExtractionCameLIGO.v

@@ -16,7 +16,6 @@ From ConCert.Execution.Test Require Import LocalBlockchain.
 From ConCert.Examples.BoardroomVoting Require Import BoardroomVotingZ.
 From Coq Require Import ZArith.
 From Coq Require Import List.
-From Coq Require Import String.
 
 Import MCMonadNotation.
 
@@ -77,7 +76,7 @@ Definition svs : list bool :=
                          (seq 0 (num_parties - votes_for)).
 
 (* Get string representation of modulus, and remap it. This way we avoid having the extraction compute the number. *)
-Definition modulus_ := StringExtra.string_of_Z modulus.
+Definition modulus_ := BytestringExtra.string_of_Z modulus.
 
 Definition init_ctx := (Chain × ContractCallContext).
 
@@ -161,7 +160,7 @@ Definition BV_MODULE : LiquidityMod msg init_ctx BV.Setup BV.State ActionBody Er
     lmd_module_name := "liquidity_boardroomvoting" ;
 
     (* definitions of operations on pairs and ints *)
-    lmd_prelude := concat nl [LiquidityPrelude; extra_ops; hash_func_def];
+    lmd_prelude := String.concat nl [LiquidityPrelude; extra_ops; hash_func_def];
 
     (* initial storage *)
     lmd_init := dummy_init;
@@ -173,9 +172,9 @@ Definition BV_MODULE : LiquidityMod msg init_ctx BV.Setup BV.State ActionBody Er
     lmd_receive := dummy_receive;
 
     (* code for the entry point *)
-    lmd_entry_point := storage_alias ++ nl
+    lmd_entry_point := (storage_alias ++ nl
                       ++ printWrapper (PREFIX ++ "receive_wrapper") ++ nl
-                      ++ printMain |}.
+                      ++ printMain)%bs |}.
 
 Definition inline_boardroom_params : list kername :=
   [  <%% Params.H %%>
@@ -345,7 +344,7 @@ Definition TT_rename : list (string * string) :=
   ; ("nil", "[]")
   ; ("true", "true")
   ; ("false", "false")
-  ; (String.to_string (string_of_kername <%% BV.State %%>), "state") (* we add [storage] so it is printed without the prefix *)
+  ; ((string_of_kername <%% BV.State %%>), "state") (* we add [storage] so it is printed without the prefix *)
   ; ("tt", "()")
   ].
 

examples/boardroomVoting/BoardroomVotingExtractionLiquidity.v

@@ -10,7 +10,6 @@ From ConCert.Utils Require Import Automation.
 From ConCert.Execution Require Import Serializable.
 From ConCert.Execution Require Import Blockchain.
 From ConCert.Execution Require Import ResultMonad.
-From Coq Require Import String.
 From Coq Require Import Lia.
 From Coq Require Import ZArith.
 
@@ -180,7 +179,7 @@ Definition TT_rename :=
 
 Time MetaCoq Run
      (t <- liquidity_extraction PREFIX TT_remap TT_rename [] COUNTER_MODULE ;;
-      tmDefinition (String.of_string COUNTER_MODULE.(lmd_module_name)) t).
+      tmDefinition COUNTER_MODULE.(lmd_module_name) t).
 
 (* Print liquidity_counter. *)
 

examples/counter/extraction/CounterCertifiedLiquidity.v

@@ -16,7 +16,6 @@ From ConCert.Extraction Require Import Common.
 From MetaCoq.Erasure.Typed Require Import CertifyingEta.
 From Coq Require Import ZArith.
 From Coq Require Import Bool.
-From Coq Require Import String.
 
 Import MCMonadNotation.
 
@@ -124,7 +123,7 @@ Definition TT_rename : list (string * string) :=
   ; ("Z0" ,"0")
   ; ("nil", "[]")
   ; ("true", "true")
-  ; (String.to_string (string_of_kername <%% storage %%>), "storage") (* we add [storage] so it is printed without the prefix *) ].
+  ; ((string_of_kername <%% storage %%>), "storage") (* we add [storage] so it is printed without the prefix *) ].
 
 Definition COUNTER_MODULE : LiquidityMod msg _ (Z × address) storage operation Error :=
   {| (* a name for the definition with the extracted code *)
@@ -153,7 +152,7 @@ Definition COUNTER_MODULE : LiquidityMod msg _ (Z × address) storage operation
 
 Time MetaCoq Run
      (t <- liquidity_extraction PREFIX TT_remap TT_rename [] COUNTER_MODULE ;;
-      tmDefinition (String.of_string COUNTER_MODULE.(lmd_module_name)) t
+      tmDefinition COUNTER_MODULE.(lmd_module_name) t
      ).
 
 (* Print liquidity_counter. *)
@@ -244,7 +243,7 @@ Definition COUNTER_PARTIAL_EXPANDED_MODULE : LiquidityMod msg _ (Z × address) s
 
 Time MetaCoq Run
      (t <- liquidity_extraction PREFIX TT_remap TT_rename [] COUNTER_PARTIAL_EXPANDED_MODULE ;;
-      tmDefinition (String.of_string COUNTER_PARTIAL_EXPANDED_MODULE.(lmd_module_name)) t
+      tmDefinition COUNTER_PARTIAL_EXPANDED_MODULE.(lmd_module_name) t
      ).
 
 (* Print liquidity_counter_partially_applied_expanded. *)

examples/counter/extraction/CounterDepCertifiedLiquidity.v

@@ -1,7 +1,6 @@
 (** * Extraction of various contracts to CameLIGO *)
 
 From Coq Require Import ZArith.
-From Coq Require Import String.
 From MetaCoq.Template Require Import All.
 From ConCert.Embedding Require Import Notations.
 From ConCert.Embedding.Extraction Require Import PreludeExt.
@@ -14,9 +13,9 @@ From ConCert.Execution Require Import ResultMonad.
 
 Import MCMonadNotation.
 
-Local Open Scope string_scope.
 Open Scope Z.
 
+
 #[local]
 Existing Instance PrintConfShortNames.PrintWithShortNames.
 
@@ -100,7 +99,7 @@ End Counter.
 Section CounterExtraction.
   Import Counter.
   (** A translation table for definitions we want to remap. The corresponding top-level definitions will be *ignored* *)
-  Definition TT_remap_counter : list (kername * String.string) :=
+  Definition TT_remap_counter : list (kername * string) :=
     [ remap <%% Z %%> "int"
     ; remap <%% Z.add %%> "addInt"
     ; remap <%% Z.sub %%> "subInt"
@@ -140,6 +139,6 @@ Section CounterExtraction.
 
   (** We redirect the extraction result for later processing and compiling with the CameLIGO compiler *)
   Redirect "cameligo-extract/CounterCertified.mligo"
-  MetaCoq Run (tmMsg (String.of_string cameLIGO_counter_1)).
+  MetaCoq Run (tmMsg cameLIGO_counter_1).
 
 End CounterExtraction.