Skip to main content

Browse the archive

https://github.com/EasyCrypt/easycrypt
09 March 2024, 04:34:05 UTC
Revision c5f30c87be0a2918bbd81970ab03f3feb36c3000 authored by Alley Stoughton on 08 March 2024, 23:54:43 UTC, committed by GitHub on 08 March 2024, 23:54:43 UTC 
Added example usage of well-founded recursion and induction (#518)
 
to examples directory. Cleaned up various things in WF.ec,
including standardizing some terminology.
1 parent a8274fe
Raw File
Tip revision: c5f30c87be0a2918bbd81970ab03f3feb36c3000 authored by Alley Stoughton on 08 March 2024, 23:54:43 UTC
Added example usage of well-founded recursion and induction (#518)
Tip revision: c5f30c8
default.nix 
{ withProvers ? false, devDeps ? [] }:

with import <nixpkgs> {};

let provers =
  if withProvers then [
    alt-ergo
    cvc4
    cvc5
    z3
  ] else []; in

stdenv.mkDerivation {
  pname = "easycrypt";
  version = "git";
  src = ./.;

  buildInputs = [ git ] ++ (with ocamlPackages; [
    ocaml
    findlib
    batteries
    camlp-streams
    dune_3
    dune-build-info
    dune-site
    inifiles
    menhir
    menhirLib
    yojson
    why3
    zarith
  ]);

  propagatedBuildInputs = devDeps ++ provers;

  installPhase = ''
    runHook preInstall
    dune install --prefix $out -p $pname
    runHook postInstall
  '';
}
back to top