Skip to content

Bump extraction dependencies #269

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
4ever2 merged 4 commits into from
May 26, 2025
Merged

Bump extraction dependencies #269

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
9b4dadd
Bump extraction dependencies
4ever2 May 23, 2025
a1bcad5
Switch to bytestrings in extraction
4ever2 May 23, 2025
e0ac1d6
Switch to bytestrings in extraction examples
4ever2 May 23, 2025
30d2a32
Fix stackinterpreter extraction
4ever2 May 26, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 2 additions & 6 deletions .github/coq-concert.opam.locked
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
155 changes: 81 additions & 74 deletions .github/workflows/nix-action-8.20.yml
View file
Open in desktop

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions .nix/config.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 = {};
Expand Down
2 changes: 1 addition & 1 deletion .nix/coq-nix-toolbox.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
"a1f630a232a3e2c739df99d0a947bf7465d2f8bb"
"944779fa54c48b734298bf78bd71a22eee0abe96"
9 changes: 2 additions & 7 deletions coq-concert.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}
]
12 changes: 5 additions & 7 deletions examples/boardroomVoting/BoardroomVotingExtractionCameLIGO.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down Expand Up @@ -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).

Expand Down Expand Up @@ -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;
Expand All @@ -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"
|}.
Expand Down Expand Up @@ -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", "()")
].

Expand All @@ -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).
11 changes: 5 additions & 6 deletions examples/boardroomVoting/BoardroomVotingExtractionLiquidity.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -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).

Expand Down Expand Up @@ -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;
Expand All @@ -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 %%>
Expand Down Expand Up @@ -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", "()")
].

Expand Down
3 changes: 1 addition & 2 deletions examples/counter/extraction/CounterCertifiedLiquidity.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -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. *)

Expand Down
7 changes: 3 additions & 4 deletions examples/counter/extraction/CounterDepCertifiedLiquidity.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -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 *)
Expand Down Expand Up @@ -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. *)
Expand Down Expand Up @@ -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. *)
Expand Down
7 changes: 3 additions & 4 deletions examples/counter/extraction/CounterLIGO.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
Expand All @@ -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.

Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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.
11 changes: 5 additions & 6 deletions examples/counter/extraction/CounterRefTypesMidlang.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,11 +12,10 @@ From MetaCoq.Common Require Import Kernames.
From MetaCoq.Template Require Import All.
From Coq Require Import List.
From Coq Require Import Lia.
From Coq Require Import String.
From Coq Require Import ZArith.

Import MCMonadNotation.
Open Scope string.


#[local]
Instance MidlangBoxes : ElmPrintConfig :=
Expand Down Expand Up @@ -154,7 +153,7 @@ Definition counter_result :=
ret lines).

Definition wrap_in_delimiters s :=
concat Common.nl [""; "{-START-} "; s; "{-END-}"].
String.concat Common.nl [""; "{-START-} "; s; "{-END-}"].

Definition midlang_prelude :=
["import Basics exposing (..)";
Expand All @@ -168,13 +167,13 @@ Definition midlang_prelude :=

MetaCoq Run (match counter_result with
| Ok s => tmMsg "Extraction of counter succeeded"%bs
| Err err => tmFail (String.of_string err)
| Err err => tmFail err
end).

Definition midlang_counter :=
match counter_result with
| Ok s => monad_map tmMsg (map String.of_string (midlang_prelude ++ s))
| Err s => tmFail (String.of_string s)
| Ok s => monad_map tmMsg (midlang_prelude ++ s)
| Err s => tmFail s
end.

Redirect "midlang-extract/CounterRefTypesMidlang.midlang"
Expand Down
3 changes: 1 addition & 2 deletions examples/counter/extraction/CounterRust.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,9 @@ From ConCert.Extraction Require Import Common.
From ConCert.Extraction Require Import ConcordiumExtract.
From RustExtraction Require Import RustExtract.
From Coq Require Import Bool.
From Coq Require Import String.
From MetaCoq.Template Require Import All.

Open Scope string.


Definition COUNTER_MODULE : ConcordiumMod _ _ :=
{| concmd_contract_name := "counter"%bs;
Expand Down
3 changes: 1 addition & 2 deletions examples/counter/extraction/CounterSubsetTypesLIGO.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ From ConCert.Execution Require Import Blockchain.
From ConCert.Execution Require Import ResultMonad.
From Coq Require Import ZArith.
From Coq Require Import Bool.
From Coq Require Import String.
From Coq Require Import Lia.

Import MCMonadNotation.
Expand Down Expand Up @@ -149,6 +148,6 @@ Module CameLIGOExtractionSetup.
Time Definition cameLIGO_counter := Eval vm_compute in cameligo_counter_prepared.

Redirect "cameligo-extract/CounterSubsetTypes.mligo"
MetaCoq Run (tmMsg (String.of_string cameLIGO_counter)).
MetaCoq Run (tmMsg cameLIGO_counter).

End CameLIGOExtractionSetup.
9 changes: 4 additions & 5 deletions examples/counter/extraction/CounterSubsetTypesLiquidity.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ From ConCert.Execution Require Import Blockchain.
From ConCert.Execution Require Import ResultMonad.
From Coq Require Import ZArith.
From Coq Require Import Bool.
From Coq Require Import String.
From Coq Require Import Lia.

Import MCMonadNotation.
Expand Down Expand Up @@ -123,14 +122,14 @@ Section LiquidityExtractionSetup.
; ("nil", "[]")
; ("true", "true")
; ("exist", "exist_") (* remapping [exist] to the wrapper *)
; (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 storage ActionBody Error :=
{| (* a name for the definition with the extracted code *)
lmd_module_name := "liquidity_counter" ;

(* definitions of operations on pairs and ints *)
lmd_prelude := concat nl [prod_ops; int_ops; sig_def; exist_def; result_def];
lmd_prelude := String.concat nl [prod_ops; int_ops; sig_def; exist_def; result_def];

(* initial storage *)
lmd_init := init ;
Expand All @@ -153,11 +152,11 @@ Section LiquidityExtractionSetup.

Time MetaCoq Run
(t <- liquidity_extraction PREFIX TT_remap TT_rename to_inline COUNTER_MODULE ;;
tmDefinition (String.of_string COUNTER_MODULE.(lmd_module_name)) t
tmDefinition COUNTER_MODULE.(lmd_module_name) t
).

(** We redirect the extraction result for later processing and compiling with the Liquidity compiler*)
Redirect "liquidity-extract/CounterSubsetTypes.liq"
MetaCoq Run (tmMsg (String.of_string liquidity_counter)).
MetaCoq Run (tmMsg liquidity_counter).

End LiquidityExtractionSetup.
Loading