Fix rendering of vertical vectors (#954)

* Use agdaWithPackages on mkdocs derivation

* Remove deduplication of package list for mkdocs dependencies

* Rename fls-agda executable to agda

Author: carlostome

build-tools/agda/flake.nix

@@ -28,7 +28,7 @@
         };
       in
       {
-        packages.default = pkgs.agda;
+        packages.default = pkgs.agdaPackages.agda;
       }
     )
     // {

build-tools/agda/fls-agda.cabal

@@ -11,7 +11,7 @@ extra-doc-files:    README.md
 data-files: data/Agda.css
             data/AgdaKaTeX.js
 
-executable fls-agda
+executable agda
   hs-source-dirs:      src
   main-is:             Main.hs
   other-modules:       Paths_fls_agda

build-tools/agda/nix/fls-agda.nix

@@ -37,5 +37,5 @@ mkDerivation {
   ];
   description = "Custom backend for formal-ledger-specifications";
   license = "unknown";
-  mainProgram = "fls-agda";
+  mainProgram = "agda";
 }

build-tools/nix/mkdocs.nix

@@ -1,10 +1,11 @@
 {
   lib,
   mkDerivation,
-  agda,
+  dejavu_fonts,
+  ghostscript,
   pandoc,
   python3,
-  ghostscript,
+  texlive,
 }:
 mkDerivation {
   pname = "mkdocs";
@@ -23,7 +24,6 @@ mkDerivation {
   };
   meta = { };
   buildInputs = [
-    agda
     pandoc
     (python3.withPackages (
       ps: with ps; [
@@ -32,8 +32,26 @@ mkDerivation {
         mkdocs-material
         pymdown-extensions
         pyyaml
+        pybtex
       ]
     ))
+    (texlive.combine {
+      inherit (texlive)
+        bclogo
+        scheme-small
+        dejavu
+        mdframed
+        zref
+        luatex
+        luatex85
+        dvisvgm
+        needspace
+        standalone
+        tikz-cd
+        pgfplots
+        ;
+    })
+    dejavu_fonts
     ghostscript
   ];
   buildPhase = ''

flake.nix

@@ -67,6 +67,7 @@
                 version = "0.1";
                 meta = args.meta or { };
                 buildInputs = (args.buildInputs or [ ]) ++ [
+                  agdaWithPackages
                   fls-shake
                   nixpkgs.agdaPackages.formal-ledger
                 ];
@@ -95,12 +96,7 @@
 
           devShells = with nixpkgs; {
             default = mkShell {
-              packages = [
-                agdaWithPackages
-                fls-shake
-                python3
-                coreutils
-              ];
+              inputsFrom = builtins.attrValues pkgs;
             };
 
             # Minimal environment for CI builds (see GH actions)
@@ -112,43 +108,8 @@
 
             # Complete documentation pipeline (mkdocs)
             mkdocs = mkShell {
-              packages = [
-                # Core Agda development
-                agdaWithPackages
-                fls-shake
-
-                # Document conversion tools
-                pandoc
-                (texlive.combine {
-                  inherit (texlive)
-                    scheme-small
-                    dejavu
-                    luatex
-                    luatex85
-                    dvisvgm
-                    standalone
-                    tikz-cd
-                    pgfplots
-                    ;
-                })
-                dejavu_fonts
-
-                # Python environment for mkdocs pipeline
-                (python3.withPackages (
-                  ps: with ps; [
-                    pip
-                    mkdocs
-                    mkdocs-material
-                    pymdown-extensions
-                    pyyaml
-                    pybtex
-                  ]
-                ))
-
-                # Additional tools
-                coreutils
-                hpack
-                ghostscript
+              inputsFrom = [
+                pkgs.mkdocs
               ];
             };
           };

src/Ledger/Conway/Specification/Certs.lagda.md

@@ -583,7 +583,10 @@ The `POST-CERT`{.AgdaFunction} transition rule is applied at the end of the
 data _⊢_⇀⦇_,POST-CERT⦈_ : CertEnv → CertState → ⊤ → CertState → Type where
 
   CERT-post :
-    ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards ⟧ , stᵖ , stᵍ ⟧ ⇀⦇ _ ,POST-CERT⦈ ⟦ ⟦ voteDelegs ∣^ (mapˢ vDelegCredential (dom (DRepsOf stᵍ)) ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ [])) , stakeDelegs , rewards ⟧ , stᵖ , stᵍ ⟧
+    let activeVDelegs = mapˢ vDelegCredential (dom (DRepsOf stᵍ))
+                         ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ [])
+    in
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards ⟧ , stᵖ , stᵍ ⟧ ⇀⦇ _ ,POST-CERT⦈ ⟦ ⟦ voteDelegs ∣^ activeVDelegs , stakeDelegs , rewards ⟧ , stᵖ , stᵍ ⟧
 
 _⊢_⇀⦇_,CERTS⦈_  : CertEnv → CertState  → List DCert  → CertState  → Type
 _⊢_⇀⦇_,CERTS⦈_ = RunTraceAfterAndThen _⊢_⇀⦇_,PRE-CERT⦈_ _⊢_⇀⦇_,CERT⦈_ _⊢_⇀⦇_,POST-CERT⦈_