Nixify + add to website

Author: amesgen

docs/agda-spec/.gitignore

@@ -5,9 +5,7 @@
 result*
 
 *.pdf
-src/latex/Ledger/*
-src/latex/MidnightExample/*
-src/latex/bclogo.sty
+src/latex/
 
 dist/
 

docs/agda-spec/flake.nix

@@ -1,4 +1,3 @@
 *.lof
 !consensus-spec.bbl
 !rules.pdf
-

docs/agda-spec/shell.nix

@@ -8,7 +8,7 @@ The following artifacts influence and/or describe the Consensus implementation.
     * [Ouroboros Praos][ouroboros-praos]
     * [Ouroboros Genesis][ouroboros-genesis]
 * [Ledger specifications][cardano-ledger].
-* [Consensus (Praos) specification](/pdfs/consensus-spec.pdf)
+* Consensus (Praos) specification: [Agda style](/pdfs/consensus-spec-agda.pdf), [LaTeX style](/pdfs/consensus-spec.pdf)
 * [Quick reference table for all Cardano features](https://github.com/cardano-foundation/CIPs/blob/master/CIP-0059/feature-table.md).
   This includes the dates and first slot numbers of all eras and hard forks.
 * IOG media:

docs/agda-spec/src/.gitignore

@@ -31,6 +31,7 @@
       url = "github:nix-community/flake-compat";
       flake = false;
     };
+    agda-nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
     # for cabal-docspec
     cabal-extras = {
       url = "github:phadej/cabal-extras/cabal-docspec-0.0.0.20240703";
@@ -63,7 +64,8 @@
             inputs.iohkNix.overlays.haskell-nix-extra
             (import ./nix/tools.nix inputs)
             (import ./nix/haskell.nix inputs)
-            (import ./nix/pdfs.nix)
+            (import ./nix/agda.nix inputs)
+            (import ./nix/pdfs.nix inputs)
           ];
         };
         hydraJobs = import ./nix/ci.nix { inherit inputs pkgs; };
@@ -76,6 +78,8 @@
           ghc910 = hydraJobs.native.haskell910.devShell;
           ghc910-profiled = hydraJobs.native.haskell910.devShellProfiled;
 
+          agda-spec = pkgs.agda-spec.shell;
+
           website = pkgs.mkShell {
             packages = [ pkgs.nodejs pkgs.yarn ];
           };

docs/website/contents/about-ouroboros/References.md

@@ -1,31 +1,26 @@
-{ sources ? import ./nix/sources.nix
-, pkgs ? import sources.nixpkgs {
-    overlays = [ ];
-    config = { };
-  }
-}:
+inputs: final: prev:
 
-with pkgs;
 let
+  pkgs = final;
+
   locales = {
     LANG = "en_US.UTF-8";
     LC_ALL = "en_US.UTF-8";
-    LOCALE_ARCHIVE = if pkgs.system == "x86_64-linux"
-                     then "${pkgs.glibcLocales}/lib/locale/locale-archive"
-                     else "";
+    LOCALE_ARCHIVE =
+      if pkgs.system == "x86_64-linux"
+      then "${pkgs.glibcLocales}/lib/locale/locale-archive"
+      else "";
   };
 
-  customAgda = import sources.agda-nixpkgs {
-    inherit (pkgs) system;
-  };
+  customAgda = inputs.agda-nixpkgs.legacyPackages.${pkgs.system};
 
   agdaStdlib = customAgda.agdaPackages.standard-library;
 
   agdaStdlibClasses = customAgda.agdaPackages.mkDerivation {
     inherit (locales) LANG LC_ALL LOCALE_ARCHIVE;
     pname = "agda-stdlib-classes";
     version = "2.0";
-    src = fetchFromGitHub {
+    src = pkgs.fetchFromGitHub {
       repo = "agda-stdlib-classes";
       owner = "omelkonian";
       rev = "v2.0";
@@ -41,7 +36,7 @@ let
     inherit (locales) LANG LC_ALL LOCALE_ARCHIVE;
     pname = "agda-stdlib-meta";
     version = "2.0";
-    src = fetchFromGitHub {
+    src = pkgs.fetchFromGitHub {
       repo = "stdlib-meta";
       owner = "input-output-hk";
       rev = "4fc4b1ed6e47d180516917d04be87cbacbf7d314";
@@ -56,33 +51,29 @@ let
   deps = [ agdaStdlib agdaStdlibClasses agdaStdlibMeta ];
   agdaWithPkgs = p: customAgda.agda.withPackages { pkgs = p; ghc = pkgs.ghc; };
 
-in
-rec {
+  attrs = pkgs.recurseIntoAttrs rec {
+    agda = agdaWithPkgs deps;
 
-  agdaWithDeps = agdaWithPkgs deps;
-  agda = agdaWithPkgs deps;
-
-  latex = texlive.combine {
-    inherit (texlive)
-      scheme-small
-      xits
-      collection-latexextra
-      collection-latexrecommended
-      collection-mathscience
-      bclogo
-      latexmk;
-  };
+    latex = pkgs.texlive.combine {
+      inherit (pkgs.texlive)
+        scheme-small
+        xits
+        collection-latexextra
+        collection-latexrecommended
+        collection-mathscience
+        bclogo
+        latexmk;
+    };
 
-  mkSpecDerivation = { project, main }: rec {
-    docs = stdenv.mkDerivation {
+    docs = pkgs.stdenv.mkDerivation {
       inherit (locales) LANG LC_ALL LOCALE_ARCHIVE;
       pname = "docs";
       version = "0.1";
-      src = "${formalLedger}";
+      src = ../docs/agda-spec;
       meta = { };
-      buildInputs = [ agdaWithDeps latex python3 ];
+      buildInputs = [ agda latex pkgs.python3 ];
       buildPhase = ''
-        OUT_DIR=$out make "${project}".docs
+        OUT_DIR=$out make docs
       '';
       doCheck = true;
       checkPhase = ''
@@ -91,7 +82,9 @@ rec {
       dontInstall = true;
     };
 
-    hsExe = haskell.lib.disableLibraryProfiling (haskellPackages.callCabal2nixWithOptions "${project}" "${hsSrc}/haskell/${main}" "--no-haddock" {});
-
+    shell = pkgs.mkShell {
+      packages = [ agda latex ];
+    };
   };
-}
+in
+{ agda-spec = attrs; }

flake.lock

@@ -40,7 +40,7 @@ let
       haskell96 = mkHaskellJobsFor pkgs.hsPkgs;
     } // lib.optionalAttrs (buildSystem == "x86_64-linux") {
       formatting = import ./formatting.nix pkgs;
-      inherit (pkgs) consensus-pdfs;
+      inherit (pkgs) consensus-pdfs agda-spec;
 
       # ensure we can still build on 8.10, can be removed soon
       haskell810 = builtins.removeAttrs

flake.nix

@@ -1,4 +1,4 @@
-final: prev: {
+inputs: final: prev: {
   consensus-pdfs = final.stdenvNoCC.mkDerivation {
     name = "ouroboros-consensus-pdfs";
     src = ../docs;
@@ -35,6 +35,7 @@ final: prev: {
 
       cp tech-reports/**/*.pdf $out/
       cp formal-spec/consensus-spec.pdf $out/
+      cp ${final.agda-spec.docs}/pdfs/consensus-spec.pdf $out/consensus-spec-agda.pdf
 
       mkdir -p $out/nix-support
       for pdf in $out/*.pdf; do