Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/main' into protz_poly_array
Browse files Browse the repository at this point in the history
  • Loading branch information
msprotz committed Nov 22, 2024
2 parents 467bed5 + 4cc8626 commit bb94c01
Showing 5 changed files with 25 additions and 88 deletions.
20 changes: 0 additions & 20 deletions .github/workflows/latest.yaml

This file was deleted.

26 changes: 10 additions & 16 deletions .github/workflows/nix.yaml
Original file line number Diff line number Diff line change
@@ -34,22 +34,16 @@ jobs:
steps:
- uses: actions/checkout@v4
- run: |
# Flake overrides aren't recursive: if I want to use eurydice with
# all its dependencies, I must override each of them.
# Flake overrides aren't recursive: if we want to use eurydice with
# any newly pinned dependencies, we must override all of them.
EURYDICE_REV="${{ github.sha }}"
CHARON_REV="$(nix develop '.#ci' --command jq -r .nodes.charon.locked.rev flake.lock)"
KRML_REV="$(nix develop '.#ci' --command jq -r .nodes.karamel.locked.rev flake.lock)"
FSTAR_REV="$(nix develop '.#ci' --command jq -r .nodes.fstar.locked.rev flake.lock)"
git clone https://github.com/cryspen/libcrux
cd libcrux
nix develop --command cargo generate-lockfile
nix build --refresh -L '.#ml-kem' \
--override-input eurydice github:aeneasverif/eurydice/${{ github.sha }} \
--override-input charon github:aeneasverif/charon/$CHARON_REV \
--override-input karamel github:FStarLang/karamel/$KRML_REV \
--override-input fstar github:FStarLang/fstar/$FSTAR_REV \
--override-input eurydice/charon github:aeneasverif/charon/$CHARON_REV \
--override-input eurydice/karamel github:FStarLang/karamel/$KRML_REV \
--override-input eurydice/fstar github:FStarLang/fstar/$FSTAR_REV \
--update-input charon/rust-overlay \
--update-input hax \
--update-input crane
git clone https://github.com/Inria-Prosecco/circus-green
cd circus-green
nix flake lock --override-input charon github:aeneasverif/charon/$CHARON_REV
nix flake lock --override-input eurydice github:aeneasverif/eurydice/$EURYDICE_REV
nix flake lock --override-input eurydice/karamel github:FStarLang/karamel/$KRML_REV
nix flake lock --override-input eurydice/karamel/fstar github:FStarLang/fstar/$FSTAR_REV
./check.sh ml-kem-small
52 changes: 9 additions & 43 deletions flake.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

11 changes: 4 additions & 7 deletions flake.nix
Original file line number Diff line number Diff line change
@@ -1,9 +1,7 @@
{
inputs = {
flake-utils.url = "github:numtide/flake-utils";
karamel.url = "github:FStarLang/karamel";
fstar.follows = "karamel/fstar";

flake-utils.follows = "karamel/flake-utils";
nixpkgs.follows = "karamel/nixpkgs";

charon.url = "github:AeneasVerif/charon";
@@ -20,14 +18,13 @@
pkgs = import nixpkgs { inherit system; };

karamel = inputs.karamel.packages.${system}.default;
fstar = inputs.karamel.inputs.fstar.packages.${system}.default;
krml = karamel.passthru.lib;

charon-packages = inputs.charon.packages.${system};
charon-ml = charon-packages.charon-ml;
charon = charon-packages.default;

fstar = inputs.fstar.packages.${system}.default;

package =
{ ocamlPackages
, removeReferencesTo
@@ -59,10 +56,10 @@
name = "tests";
src = ./.;
KRML_HOME = karamel;
FSTAR_HOME = fstar;
FSTAR_HOME = "dummy";
EURYDICE = "${eurydice}/bin/eurydice";
buildInputs = [ charon.buildInputs eurydice ];
nativeBuildInputs = [ charon.nativeBuildInputs fstar clang ];
nativeBuildInputs = [ charon.nativeBuildInputs clang ];
buildPhase = ''
export CHARON="${charon}/bin/charon"
4 changes: 2 additions & 2 deletions lib/AstOfLlbc.ml
Original file line number Diff line number Diff line change
@@ -1646,7 +1646,7 @@ let decl_of_id (env : env) (id : C.any_decl_id) : K.decl option =
match decl with
| None -> None
| Some decl -> (
let { C.def_id; signature; body; is_global_decl_body; item_meta; kind; _ } = decl in
let { C.def_id; signature; body; item_meta; kind; _ } = decl in
let env = { env with generic_params = signature.generics } in
L.log "AstOfLlbc" "Visiting %sfunction: %s\n%s"
(if body = None then
@@ -1668,7 +1668,7 @@ let decl_of_id (env : env) (id : C.any_decl_id) : K.decl option =
let { K.n_cgs; n }, t = typ_of_signature env signature in
Some (K.DExternal (None, [], n_cgs, n, name, t, []))
| Some { locals; body; _ }, _ ->
if is_global_decl_body then
if Option.is_some decl.is_global_initializer then
None
else
let env = push_cg_binders env signature.C.generics.const_generics in

0 comments on commit bb94c01

Please sign in to comment.