merge master into dijkstra-dev

.github/workflows/build_artifact.yml

@@ -21,10 +21,10 @@ jobs:
           extra_nix_config: |
             trusted-public-keys = hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
             substituters = https://cache.iog.io https://cache.nixos.org/
-      - name: Build the target ${{ inputs.target }}
+      - name: Build artifact
         run: |
-          nix-shell --run 'fls-shake --trace -j8 ${{ inputs.target }}'
-      - name: Upload ${{ inputs.target }} artifact
+          nix-shell -A devShells.ci --run 'fls-shake --trace -j8 ${{ inputs.target }}'
+      - name: Upload artifact
         uses: actions/upload-artifact@v4
         with:
           name: ${{ inputs.target }}

.github/workflows/build.yml → .github/workflows/ci.yml

@@ -1,8 +1,9 @@
-name: Build and upload artifacts
+name: CI
 on:
   push:
     branches:
     - master
+    - legacy-latex  # ensure legacy-latex-artifacts branch gets created
   pull_request:
     branches:
     - master
@@ -24,10 +25,10 @@ jobs:
           extra_nix_config: |
             trusted-public-keys = hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
             substituters = https://cache.iog.io https://cache.nixos.org/
-      - name: Build formalLedger
-        id: formalLedger
+      - name: Build formal-ledger
+        id: formal-ledger
         run: |
-          nix-build -A formalLedger -o outputs
+          nix-build -A formal-ledger -o outputs
       - name: Upload agda _build artifact
         uses: actions/upload-artifact@v4
         with:
@@ -45,28 +46,78 @@ jobs:
     with:
       target: hs
 
-  cardano-ledger-pdf:
+  hs-build:
+    needs: [hs]
+    runs-on: ubuntu-latest
+    steps:
+      - name: Download extracted Haskell code
+        uses: actions/download-artifact@v4
+        with:
+          name: hs
+          path: dist
+      - name: Install Nix
+        uses: cachix/install-nix-action@v31
+        with:
+          nix_path: nixpkgs=https://github.com/NixOS/nixpkgs/archive/6c5963357f3c1c840201eda129a99d455074db04.tar.gz
+          extra_nix_config: |
+            trusted-public-keys = hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
+            substituters = https://cache.iog.io https://cache.nixos.org/
+      - name: Build the extracted Haskell code
+        run: |
+          nix-shell -p haskell.compiler.ghc96 cabal-install --run "cd dist/hs; cabal update && cabal build"
+
+  html:
     needs: [formal-ledger-agda]
     uses: ./.github/workflows/build_artifact.yml
     with:
-      target: cardano-ledger.pdf
+      target: html
 
-  conway-ledger-pdf:
+  mkdocs-site:
     needs: [formal-ledger-agda]
-    uses: ./.github/workflows/build_artifact.yml
+    # # Should we only run on master branch? If so, uncomment next line.
+    # if: ${{ github.ref_name == 'master' }}
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout main repository
+        uses: actions/checkout@v4
+      - name: Download agda _build artifact
+        uses: actions/download-artifact@v4
+        with:
+          name: _build
+          path: _build
+      - name: Install Nix
+        uses: cachix/install-nix-action@v31
+        with:
+          nix_path: nixpkgs=https://github.com/NixOS/nixpkgs/archive/6c5963357f3c1c840201eda129a99d455074db04.tar.gz
+          extra_nix_config: |
+            trusted-public-keys = hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
+            substituters = https://cache.iog.io https://cache.nixos.org/
+      - name: Generate and Build MkDocs site
+        run: |
+          nix-build -A mkdocs -o outputs
+      - name: Upload MkDocs site artifact
+        uses: actions/upload-artifact@v4
+        with:
+          name: mkdocs-site
+          path: outputs
+
+  cardano-ledger-pdf:
+    needs: [formal-ledger-agda]
+    uses: ./.github/workflows/copy_legacy_pdf.yml
     with:
-      target: conway-ledger.pdf
+      pdf_name: cardano-ledger.pdf
 
-  html:
+  conway-ledger-pdf:
     needs: [formal-ledger-agda]
-    uses: ./.github/workflows/build_artifact.yml
+    uses: ./.github/workflows/copy_legacy_pdf.yml
     with:
-      target: html
+      pdf_name: conway-ledger.pdf
 
-  upload-artifacts:
-    # This job runs only if the workflow has not been manually dispached
-    if: ${{ github.event_name != 'workflow_dispatch' }}
-    needs: [formal-ledger-agda, hs, conway-ledger-pdf, cardano-ledger-pdf, html]
+  push-artifacts-to-branch:
+    # This job runs only if the workflow has not been manually dispached,
+    # and the origininating branch belongs to the repository
+    if: ${{ github.event_name != 'workflow_dispatch' && ! github.event.pull_request.head.repo.fork }}
+    needs: [formal-ledger-agda, hs, hs-build, html, conway-ledger-pdf, cardano-ledger-pdf, mkdocs-site]
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
@@ -81,13 +132,12 @@ jobs:
             echo "artifacts_branch=${{ github.event.pull_request.head.ref }}-artifacts" >> $GITHUB_OUTPUT
             printf "artifacts_branch: %s\n" "${{ github.event.pull_request.head.ref }}-artifacts"
           else
-            printf "This workflow was triggered by a push event to master\n"
-            echo "artifacts_branch=master-artifacts" >> $GITHUB_OUTPUT
-            printf "artifacts_branch: %s\n" "master-artifacts"
+            printf "This workflow was triggered by a push event to ${{ github.ref_name }}\n"
+            echo "artifacts_branch=${{ github.ref_name }}-artifacts" >> $GITHUB_OUTPUT
+            printf "artifacts_branch: %s\n" "${{ github.ref_name }}-artifacts"
           fi
-      # Checkout env.artifacts_branch if it already exists
-      # otherwise create a new orphan branch.
-      # Lastly, remove all files from the repo
+      # Checkout env.artifacts_branch if it already exists otherwise create a new orphan branch.
+      # Lastly, remove all files from the repo.
       - name: Checkout artifacts branch
         run: |
           if [[ -n "$(git ls-remote --heads origin "${ARTIFACTS_BRANCH}")" ]]; then
@@ -142,7 +192,7 @@ jobs:
           cat << EOF >> index.html
           	<hr>
           	<p class="VERSION">
-              Automatically generated from commit <a href="https://github.com/intersectmbo/formal-ledger-specifications/commit/${{ github.sha }}">${{ github.sha }}</a>
+              Automatically generated from commit <a href="https://github.com/intersectmbo/formal-ledger-specifications/commit/${{ github.sha }}">${{ github.sha }}</a> on branch ${{ github.ref_name }}
           	</p>
           </body>
           </html>
@@ -153,7 +203,7 @@ jobs:
             git config user.name 'github-actions[bot]'
             git config user.email 'github-actions[bot]@users.noreply.github.com'
             git add -A
-            git commit -m "Artifacts generated from ${{ github.sha }}"
+            git commit --allow-empty -m "Artifacts generated from ${{ github.sha }}"
       - name: Push ${{ env.artifacts_branch }}
         uses: ad-m/[email protected]
         with:
@@ -163,7 +213,7 @@ jobs:
 
   build-cardano-ledger:
     needs: [hs]
-    if: ${{ github.event_name == 'push' }}
+    if: ${{ github.event_name == 'push' || github.event_name == 'workflow_dispatch' }}
     runs-on: ubuntu-latest
     steps:
       - uses: cachix/install-nix-action@v31
@@ -176,7 +226,7 @@ jobs:
         uses: actions/checkout@v4
         with:
           sparse-checkout: |
-            scripts/prepare-conf-test.sh
+            build-tools/scripts/prepare-conf-test.sh
           sparse-checkout-cone-mode: false
           path: fls
 
@@ -195,4 +245,4 @@ jobs:
       - name: Build cardano-ledger
         run: |
           cd cl
-          nix develop --command bash -c "../fls/scripts/prepare-conf-test.sh . ../hs && cabal update && cabal build cardano-ledger-conformance"
+          nix develop --command bash -c "../fls/build-tools/scripts/prepare-conf-test.sh . ../hs && cabal update && cabal build cardano-ledger-conformance"

.github/workflows/copy_legacy_pdf.yml

@@ -0,0 +1,70 @@
+on:
+  workflow_call:
+    inputs:
+      pdf_name:
+        required: true
+        type: string
+        description: 'Name of the PDF file to copy (e.g., cardano-ledger.pdf)'
+
+jobs:
+  copy-legacy-pdf:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout current branch
+        uses: actions/checkout@v4
+
+      - name: Copy PDF from legacy-latex-artifacts branch
+        run: |
+          echo "📄 Attempting to copy ${{ inputs.pdf_name }} from legacy-latex-artifacts branch..."
+
+          # Check if legacy-latex-artifacts branch exists
+          if ! git ls-remote --exit-code --heads origin legacy-latex-artifacts > /dev/null 2>&1; then
+            echo "❌ FATAL: legacy-latex-artifacts branch does not exist"
+            echo ""
+            echo "This branch is required to provide legacy PDF files for the documentation."
+            echo ""
+            echo "Expected file: ${{ inputs.pdf_name }}"
+            echo "Expected branch: legacy-latex-artifacts"
+            echo ""
+            echo "To resolve this issue:"
+            echo "1. Ensure the legacy-latex branch exists with the original LaTeX source"
+            echo "2. Run CI on the legacy-latex branch to generate the artifacts branch"
+            echo "3. Verify that ${{ inputs.pdf_name }} exists in the legacy-latex-artifacts branch"
+            exit 1
+          fi
+
+          echo "✅ legacy-latex-artifacts branch found"
+
+          # Checkout the legacy artifacts branch
+          git fetch origin legacy-latex-artifacts:legacy-latex-artifacts
+          git checkout legacy-latex-artifacts
+
+          # Check if the specific PDF exists
+          if [ ! -f "${{ inputs.pdf_name }}" ]; then
+            echo "❌ FATAL: ${{ inputs.pdf_name }} not found in legacy-latex-artifacts branch"
+            echo ""
+            echo "Expected file: ${{ inputs.pdf_name }}"
+            echo "Available files in legacy-latex-artifacts:"
+            ls -la *.pdf 2>/dev/null || echo "  No PDF files found"
+            echo ""
+            echo "To resolve this issue:"
+            echo "1. Check that the legacy-latex branch contains the source for ${{ inputs.pdf_name }}"
+            echo "2. Re-run CI on the legacy-latex branch to regenerate artifacts"
+            echo "3. Verify that the PDF generation process completed successfully"
+            exit 1
+          fi
+
+          # Create dist directory and copy PDF
+          mkdir -p ../dist
+          cp "${{ inputs.pdf_name }}" ../dist/
+          echo "✅ Successfully copied ${{ inputs.pdf_name }}"
+
+          # Return to original branch and move the dist directory
+          git checkout -
+          mv ../dist ./dist
+
+      - name: Upload PDF artifact
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ inputs.pdf_name }}
+          path: dist

.github/workflows/shellcheck.yml

@@ -30,7 +30,7 @@ jobs:
           script: |
             printf "Checking shellcheck on all scripts.\n"
 
-            git ls-files scripts/       \
+            git ls-files build-tools/scripts/       \
               | grep '\.sh'             \
               | xargs -rd\\n -I {} -- shellcheck {}
 

.gitignore

@@ -1,7 +1,6 @@
 ## Ignore build products
 _build/
 dist
-latex/.auctex-auto
 
 ## Ignore shake folder
 .shake/
@@ -31,3 +30,17 @@ result*
 ## git-merge conflict resolution artifacts
 *.agda.orig
 *.lagda.orig
+
+## Python
+build-tools/scripts/md/__pycache__/
+__pycache__
+
+## LaTeX
+latex/.auctex-auto
+build-tools/static/latex/*.aux
+build-tools/static/latex/*.log
+build-tools/static/latex/*-Diagram.pdf
+build-tools/static/latex/*-Diagram.svg
+
+## Prevent accidental adding of conflict files!
+*.orig

CHANGELOG.md

@@ -4,6 +4,13 @@
 
 ### WIP
 
+- Add the BBODY transition relation from Shelley
+- Add the RUPD and TICK transition relations
+- Change two constructor names of `GovActionType` data type
+- Change 14 field names of `TxBody` record type
+- Implement the POOLREAP state transition relation from Shelley
+- Move `txsize` from `TxBody` to `Tx`.
+- Change the return type of `refScripts` to a set
 - Add `poolParameters` field to `Snapshot` and compute it in `SNAP`.
 - Add `treasuryCut` (formerly `tau`) and `monetaryExpansion` (formerly `rho`) to `PParams`
 - Change the `DELEG-dereg` transition so that the deposit field can be empty