Commit 92f87ee7 authored by Pierre Roux's avatar Pierre Roux
Browse files

rocqPackages.stdlib: 9.0+rc1 -> 9.0.0

parent 582a0333

pkgs/development/coq-modules/stdlib/default.nix

+10 −12
Original line number Diff line number Diff line
@@ -16,16 +16,20 @@ 
  defaultVersion =

    with lib.versions;

    lib.switch coq.version [

      { case = isEq "9.0"; out = "9.0+rc1"; }

      { case = isLt "8.21"; out = "8.20"; }

      { case = isEq "9.0"; out = "9.0.0"; }

      # the one below is artificial as stdlib was included in Coq before

      { case = isLt "9.0"; out = "9.0.0"; }

    ] null;

  releaseRev = v: "V${v}";



  release."9.0+rc1".sha256 = "sha256-raHwniQdpAX1HGlMofM8zVeXcmlUs+VJZZg5VF43k/M=";

  release."8.20".sha256 = "sha256-AcoS4edUYCfJME1wx8UbuSQRF3jmxhArcZyPIoXcfu0=";



  useDune = true;

  release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";



  configurePhase = ''

    echo no configuration

  '';

  buildPhase = ''

    echo building nothing

  '';

  installPhase = ''

    echo installing nothing

  '';
@@ -40,12 +44,6 @@ 
    o:

    # stdlib is already included in Coq <= 8.20

    if coq.version != null && coq.version != "dev" && lib.versions.isLt "8.21" coq.version then {

      configurePhase = ''

        echo no configuration

      '';

      buildPhase = ''

        echo building nothing

      '';

      installPhase = ''

        touch $out

      '';

pkgs/development/rocq-modules/stdlib/default.nix

+5 −19
Original line number Diff line number Diff line
@@ -15,29 +15,15 @@ mkRocqDerivation { 
  defaultVersion =

    with lib.versions;

    lib.switch rocq-core.version [

      { case = isEq "9.0"; out = "9.0+rc1"; }

      { case = isLt "8.21"; out = "8.20"; }

      { case = isEq "9.0"; out = "9.0.0"; }

      # the one below is artificial as stdlib was included in Coq before

      { case = isLt "9.0"; out = "9.0.0"; }

    ] null;

  releaseRev = v: "V${v}";



  release."9.0+rc1".sha256 = "sha256-raHwniQdpAX1HGlMofM8zVeXcmlUs+VJZZg5VF43k/M=";

  release."8.20".sha256 = "sha256-AcoS4edUYCfJME1wx8UbuSQRF3jmxhArcZyPIoXcfu0=";

  release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";



  useDune = true;



  configurePhase = ''

    patchShebangs dev/with-rocq-wrap.sh

  '';



  buildPhase = ''

    dev/with-rocq-wrap.sh dune build -p rocq-stdlib @install ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}

  '';



  installPhase = ''

    dev/with-rocq-wrap.sh dune install --root . rocq-stdlib --prefix=$out --libdir $OCAMLFIND_DESTDIR

    mkdir $out/lib/coq/

    mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${rocq-core.rocq-version}

  '';

  mlPlugin = true;



  meta = {

    description = "The Rocq Proof Assistant -- Standard Library";