Skip to content

Commit

Permalink
Modify certifier to produce new form of certificates (IntersectMBO#6734)
Browse files Browse the repository at this point in the history 
Co-authored-by: zeme <[email protected]>
  • Loading branch information
@ana-pantilie @zeme-wana
ana-pantilie and zeme-wana authored Dec 19, 2024
1 parent 8bb1a4b commit 7d20b1e
Show file tree
Hide file tree
Showing 7 changed files with 175 additions and 225 deletions.
12 changes: 0 additions & 12 deletions nix/agda.nix
View file
Original file line number Diff line number Diff line change
Expand Up @@ -115,16 +115,4 @@ rec {
cabalProjectLocal = "extra-packages: ieee754, filemanip";
modules = [ agda-project-module-patch-default ];
};

# TODO this is a bit of a hack, but it's the only way to get the uplc
# executable to find the metatheory and the stdandard library.
shell-hook-exports = ''
export AGDA_STDLIB_SRC="${agda-stdlib}/src"
export PLUTUS_METHATHEORY_SRC="./plutus-metatheory/src"
'';

wrap-program-args = ''
--set AGDA_STDLIB_SRC "${agda-stdlib}/src" \
--set PLUTUS_METHATHEORY_SRC "./plutus-metatheory/src"
'';
}
268 changes: 125 additions & 143 deletions nix/project.nix
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,151 +3,133 @@
{ repoRoot, inputs, pkgs, system, lib }:

let
cabalProject = pkgs.haskell-nix.cabalProject' ({ config, pkgs, ... }:
let
isCompilingMingwW64 = pkgs.stdenv.hostPlatform.system == "x86_64-windows"
&& pkgs.stdenv.hostPlatform.libc == "msvcrt";
isCompilingMusl64 = pkgs.stdenv.hostPlatform.system == "x86_64-linux"
&& pkgs.stdenv.hostPlatform.libc == "musl";
in {
name = "plutus";

# We need the mkDefault here since compiler-nix-name will be overridden
# in the flake variants.
compiler-nix-name = lib.mkDefault "ghc96";

src = ../.;

shell = {
withHoogle = true;
# We would expect R to be pulled in automatically as it's a dependency of
# plutus-core, but it appears it is not, so we need to be explicit about
# the dependency on R here. Adding it as a buildInput will ensure it's
# added to the pkg-config env var.
buildInputs = [ pkgs.R ];
};

flake.variants = {
ghc96 = { }; # Alias for the default project
ghc96-profiled.modules = [{
enableProfiling = true;
enableLibraryProfiling = true;
}];
ghc810.compiler-nix-name = "ghc810";
ghc98.compiler-nix-name = "ghc98";
ghc910.compiler-nix-name = "ghc910";
};

inputMap = {
"https://chap.intersectmbo.org/" = inputs.iogx.inputs.CHaP;
};

sha256map = {
"https://github.com/jaccokrijnen/plutus-cert"."e814b9171398cbdfecdc6823067156a7e9fc76a3" =
"0srqvx0b819b5crrbsa9hz2fnr50ahqizvvm0wdmyq2bbpk2rka7";
};

modules = [

(lib.mkIf (!isCompilingMingwW64 && !isCompilingMusl64)
repoRoot.nix.agda.agda-project-module-patch-default)

(lib.mkIf isCompilingMusl64
repoRoot.nix.agda.agda-project-module-patch-musl64)

# Common
{
packages = {
# plutus-metatheory needs agda with the stdlib around for the custom setup
# I can't figure out a way to apply this as a blanket change for all the
# components in the package, oh well
plutus-metatheory.components.library.build-tools =
[ repoRoot.nix.agda.agda-with-stdlib ];
plutus-metatheory.components.exes.plc-agda.build-tools =
[ repoRoot.nix.agda.agda-with-stdlib ];
plutus-metatheory.components.tests.test-NEAT.build-tools =
[ repoRoot.nix.agda.agda-with-stdlib ];

plutus-executables.components.exes.uplc.build-tools =
[ repoRoot.nix.agda.agda-with-stdlib ];
# plutus-executables.components.exes.uplc.postInstall = ''
# wrapProgram $out/bin/uplc ${repoRoot.nix.agda.wrap-program-args}
# '';

plutus-executables.components.tests.test-simple.build-tools =
[ repoRoot.nix.agda.agda-with-stdlib ];
plutus-executables.components.tests.test-detailed.build-tools =
[ repoRoot.nix.agda.agda-with-stdlib ];

plutus-core.components.benchmarks.update-cost-model = {
build-tools = [ repoRoot.nix.r-with-packages ];
};

plutus-core.components.benchmarks.cost-model-test = {
build-tools = [ repoRoot.nix.r-with-packages ];
};

plutus-cert.components.library.build-tools =
# Needs to build both itself and its bundled deps.
# This needs both coq and ocaml packages, and only
# works with particular versions. Fortunately
# they're in nixpkgs.
let
ocamlPkgs = pkgs.ocaml-ng.ocamlPackages_4_10;
coqPkgs = pkgs.coqPackages_8_13;
in with ocamlPkgs;
with coqPkgs; [
pkgs.perl
ocaml
ocamlbuild
findlib
coq
mathcomp
coq-ext-lib
ssreflect
equations
];

plutus-core.components.tests.plutus-core-test.postInstall = ''
wrapProgram $out/bin/plutus-core-test --set PATH ${
lib.makeBinPath [ pkgs.diffutils ]
}
'';

plutus-core.components.tests.plutus-ir-test.postInstall = ''
wrapProgram $out/bin/plutus-ir-test --set PATH ${
lib.makeBinPath [ pkgs.diffutils ]
}
'';

# We want to build it but not run the tests in CI.
cardano-constitution.doCheck = false;
cabalProject = pkgs.haskell-nix.cabalProject' ({ config, pkgs, ... }: {
name = "plutus";

# We need the mkDefault here since compiler-nix-name will be overridden
# in the flake variants.
compiler-nix-name = lib.mkDefault "ghc96";

src = ../.;

shell = {
withHoogle = true;
# We would expect R to be pulled in automatically as it's a dependency of
# plutus-core, but it appears it is not, so we need to be explicit about
# the dependency on R here. Adding it as a buildInput will ensure it's
# added to the pkg-config env var.
buildInputs = [ pkgs.R ];
};

flake.variants = {
ghc96 = { }; # Alias for the default project
ghc96-profiled.modules = [{
enableProfiling = true;
enableLibraryProfiling = true;
}];
ghc810.compiler-nix-name = "ghc810";
ghc98.compiler-nix-name = "ghc98";
ghc910.compiler-nix-name = "ghc910";
};

inputMap = { "https://chap.intersectmbo.org/" = inputs.iogx.inputs.CHaP; };

sha256map = {
"https://github.com/jaccokrijnen/plutus-cert"."e814b9171398cbdfecdc6823067156a7e9fc76a3" =
"0srqvx0b819b5crrbsa9hz2fnr50ahqizvvm0wdmyq2bbpk2rka7";
};

modules = [
# Common
{
packages = {
# plutus-metatheory needs agda with the stdlib around for the custom setup
# I can't figure out a way to apply this as a blanket change for all the
# components in the package, oh well
plutus-metatheory.components.library.build-tools =
[ repoRoot.nix.agda.agda-with-stdlib ];
plutus-metatheory.components.exes.plc-agda.build-tools =
[ repoRoot.nix.agda.agda-with-stdlib ];
plutus-metatheory.components.tests.test-NEAT.build-tools =
[ repoRoot.nix.agda.agda-with-stdlib ];

plutus-executables.components.exes.uplc.build-tools =
[ repoRoot.nix.agda.agda-with-stdlib ];

plutus-executables.components.tests.test-simple.build-tools =
[ repoRoot.nix.agda.agda-with-stdlib ];
plutus-executables.components.tests.test-detailed.build-tools =
[ repoRoot.nix.agda.agda-with-stdlib ];

plutus-core.components.benchmarks.update-cost-model = {
build-tools = [ repoRoot.nix.r-with-packages ];
};
}

# -Werror for CI
# Only enable on the newer compilers. We don't care about warnings on the old ones,
# and sometimes it's hard to be warning free on all compilers, e.g. the unused
# packages warning is bad in 8.10.7
# (https://gitlab.haskellib.org/ghc/ghc/-/merge_requests/6130)
(lib.mkIf (config.compiler-nix-name != "ghc8107") {
packages = {

# Werror everything.
# This is a pain, see https://github.com/input-output-hk/haskell.nix/issues/519
plutus-benchmark.ghcOptions = [ "-Werror" ];
plutus-executables.ghcOptions = [ "-Werror" ];
plutus-conformance.ghcOptions = [ "-Werror" ];
plutus-core.ghcOptions = [ "-Werror" ];
plutus-ledger-api.ghcOptions = [ "-Werror" ];
# FIXME: has warnings in generated code
#plutus-metatheory.package.ghcOptions = "-Werror";
plutus-tx.ghcOptions = [ "-Werror" ];
plutus-tx-plugin.ghcOptions = [ "-Werror" ];

plutus-core.components.benchmarks.cost-model-test = {
build-tools = [ repoRoot.nix.r-with-packages ];
};
})
];
});

plutus-cert.components.library.build-tools =
# Needs to build both itself and its bundled deps.
# This needs both coq and ocaml packages, and only
# works with particular versions. Fortunately
# they're in nixpkgs.
let
ocamlPkgs = pkgs.ocaml-ng.ocamlPackages_4_10;
coqPkgs = pkgs.coqPackages_8_13;
in with ocamlPkgs;
with coqPkgs; [
pkgs.perl
ocaml
ocamlbuild
findlib
coq
mathcomp
coq-ext-lib
ssreflect
equations
];

plutus-core.components.tests.plutus-core-test.postInstall = ''
wrapProgram $out/bin/plutus-core-test --set PATH ${
lib.makeBinPath [ pkgs.diffutils ]
}
'';

plutus-core.components.tests.plutus-ir-test.postInstall = ''
wrapProgram $out/bin/plutus-ir-test --set PATH ${
lib.makeBinPath [ pkgs.diffutils ]
}
'';

# We want to build it but not run the tests in CI.
cardano-constitution.doCheck = false;
};
}

# -Werror for CI
# Only enable on the newer compilers. We don't care about warnings on the old ones,
# and sometimes it's hard to be warning free on all compilers, e.g. the unused
# packages warning is bad in 8.10.7
# (https://gitlab.haskellib.org/ghc/ghc/-/merge_requests/6130)
(lib.mkIf (config.compiler-nix-name != "ghc8107") {
packages = {

# Werror everything.
# This is a pain, see https://github.com/input-output-hk/haskell.nix/issues/519
plutus-benchmark.ghcOptions = [ "-Werror" ];
plutus-executables.ghcOptions = [ "-Werror" ];
plutus-conformance.ghcOptions = [ "-Werror" ];
plutus-core.ghcOptions = [ "-Werror" ];
plutus-ledger-api.ghcOptions = [ "-Werror" ];
# FIXME: has warnings in generated code
#plutus-metatheory.package.ghcOptions = "-Werror";
plutus-tx.ghcOptions = [ "-Werror" ];
plutus-tx-plugin.ghcOptions = [ "-Werror" ];
};
})
];
});

project = lib.iogx.mkHaskellProject {
inherit cabalProject;
Expand Down
1 change: 0 additions & 1 deletion nix/shell.nix
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,6 @@ in {

shellHook = ''
${builtins.readFile certEnv}
${repoRoot.nix.agda.shell-hook-exports}
'';

preCommit = {
Expand Down
Loading

0 comments on commit 7d20b1e

Please sign in to comment.