Generate Haskell code from the Agda spec #1315

javierdiaz72 · 2024-11-21T12:16:43Z

This PR resolves #1312 and #1343.

javierdiaz72 · 2024-11-21T13:34:02Z

Perhaps at this point, before I move forward with other STS's, there is a good opportunity to properly integrate this work into the current Cabal project.

@amesgen: What's your opinion? Is this perhaps something you can do? (no pressure 🙂).

abailly · 2024-11-25T10:46:58Z

I have tried make hs locally, without using nix, and it fails with the following error:

    Checking Interface.HasOrder.Instance (ouroboros-consensus/docs/agda-spec/src/Interface/HasOrder/Instance.agda).
ouroboros-consensus/docs/agda-spec/src/Interface/HasOrder/Instance.agda:34,55-64
No instance of type
((HasPartialOrder.hasPreorder ℚ-hasPartialOrder HasPreorder.≤ x) y
 ⁇)
was found in scope.
when checking that the expression record {} has type
HasDecPartialOrder
make: *** [latex/Spec/PDF.tex] Error 42

I am using agda-stdlib 2.0. What am I doing wrong?

amesgen · 2024-11-25T13:54:02Z

Perhaps at this point, before I move forward with other STS's, there is a good opportunity to properly integrate this work into the current Cabal project.

@amesgen: What's your opinion? Is this perhaps something you can do? (no pressure 🙂).

Will have a look 👍

I have tried make hs locally, without using nix, and it fails with the following error:

    Checking Interface.HasOrder.Instance (ouroboros-consensus/docs/agda-spec/src/Interface/HasOrder/Instance.agda).
ouroboros-consensus/docs/agda-spec/src/Interface/HasOrder/Instance.agda:34,55-64
No instance of type
((HasPartialOrder.hasPreorder ℚ-hasPartialOrder HasPreorder.≤ x) y
 ⁇)
was found in scope.
when checking that the expression record {} has type
HasDecPartialOrder
make: *** [latex/Spec/PDF.tex] Error 42

I am using agda-stdlib 2.0. What am I doing wrong?

I am not sure exactly, but maybe you need to setup agda-stdlib-classes and agda-stdlib-meta?

ouroboros-consensus/nix/agda.nix

Lines 19 to 49 in f196bfc

    
           agdaStdlibClasses = customAgda.agdaPackages.mkDerivation { 
        
             inherit (locales) LANG LC_ALL LOCALE_ARCHIVE; 
        
             pname = "agda-stdlib-classes"; 
        
             version = "2.0"; 
        
             src = pkgs.fetchFromGitHub { 
        
               owner = "omelkonian"; 
        
               repo = "agda-stdlib-classes"; 
        
               rev = "v2.0"; 
        
               hash = "sha256-PcieRRnctjCzFCi+gUYAgyIAicMOAZPl8Sw35fZdt0E="; 
        
             }; 
        
             meta = { }; 
        
             libraryFile = "agda-stdlib-classes.agda-lib"; 
        
             everythingFile = "Classes.agda"; 
        
             buildInputs = [ agdaStdlib ]; 
        
           }; 
        
           agdaStdlibMeta = customAgda.agdaPackages.mkDerivation { 
        
             inherit (locales) LANG LC_ALL LOCALE_ARCHIVE; 
        
             pname = "agda-stdlib-meta"; 
        
             version = "2.0"; 
        
             src = pkgs.fetchFromGitHub { 
        
               owner = "omelkonian"; 
        
               repo = "agda-stdlib-meta"; 
        
               rev = "v2.1.1"; 
        
               hash = "sha256-qOoThYMG0dzjKvwmzzVZmGcerfb++MApbaGRzLEq3/4="; 
        
             }; 
        
             meta = { }; 
        
             libraryFile = "agda-stdlib-meta.agda-lib"; 
        
             everythingFile = "Main.agda"; 
        
             buildInputs = [ agdaStdlib agdaStdlibClasses ]; 
        
           };

abailly · 2024-11-25T13:57:57Z

@amesgen thanks for your answer 🙏 So I have those setup, they are in my ~/.agda/libraries definition. I will double check the versions.
Thing is: when I use nix, eg. nix develop agda, I don't seem to have the needed libraries either. It does not even bring agda into scope so I am probably misusing nix here. It would be nice to add some documentation in does/agda-spec/README.d for example to help the poor soul ending up here how to hack on these things.

abailly · 2024-11-25T14:03:29Z

It seems I had outdated version of agda-stdlib-classes and agda-stdlib-meta. Refreshing to match the revisions given in nix file does yield to different errors.

amesgen · 2024-11-25T14:06:02Z

Thing is: when I use nix, eg. nix develop agda, I don't seem to have the needed libraries either. It does not even bring agda into scope so I am probably misusing nix here. It would be nice to add some documentation in does/agda-spec/README.d for example to help the poor soul ending up here how to hack on these things.

It should work with

nix develop .#agda-spec

We definitely want a good readme for docs/agda-spec, hopefully we can get to that soon (the spec is still fairly new and evolving).

abailly · 2024-11-25T14:16:21Z

It's funny that nix develop agda-spec does not work, but nix develop agda worked although it yielded me no usable environment

amesgen · 2024-11-25T14:50:13Z

It's funny that nix develop agda-spec does not work, but nix develop agda worked although it yielded me no usable environment

Just to explain this behavior: These two commands use the Nix registry which is completely independent of the local project you are working on. Therefore, nix develop agda works because agda is a registry entry in the global flake, but agda-spec is not. However, nix develop agda will drop you in a shell that you can use to work on Agda (https://github.com/agda/agda), but this is not what you want here, in a project that uses Agda.

In contrast, nix develop .#agda-spec uses the agda-spec shell defined in the local flake (ie in . or in a parent directory):

ouroboros-consensus/flake.nix

Line 81 in 68b9799

agda-spec = pkgs.agda-spec.shell;

abailly · 2024-11-25T15:04:24Z

I still wish I could make hs without needing nix though :)

Signed-off-by: Javier Díaz <[email protected]>

Fixes #1343 Note that this PR targets the branch of #1315 and not `main`. This PR adds Nix derivations that: - generate Haskell code from the Agda spec using the `Makefile`-based build system in `./docs/agda-spec/` - wrap the generated code into Nix using `cabal2nix` In combination with the existing set-up in `flake.nix`, we can now build the generated code and run it's tests using the following flake output: ``` nix build .#hydraJobs.x86_64-linux.native.agda-spec.hsExe ``` which will also be done in CI, i.e. see the logs from testing this PR - the job [x86_64-linux.native.agda-spec.hsExe](https://ci.iog.io/build/6263029/log) builds and runs tests for the generated code some other jobs, e.g. the linting of the unit tests for the generated code, are failing, but we can fix those in #1315

…pec-to-haskell' into javierdiaz72/agda-spec-to-haskell

…nction fields

- dos2unix - hlint - make `cardano-consensus-executable-spec.cabal` pass `cabal.check` Make `cardano-consensus-executable-spec.cabal` pass `cabal.check` Copy licence files instead of linking fix cabal file

geo2a · 2025-01-13T08:07:59Z

Hi @javierdiaz72, Happy New Year! Shall we merge this PR so that it does not bit-rot?

javierdiaz72 · 2025-01-20T13:22:36Z

Hi @javierdiaz72, Happy New Year! Shall we merge this PR so that it does not bit-rot?

Hi, @geo2a! Happy New Year to you too! There is still quite a bit of work to do regarding this PR (that's why it's still in draft mode), so we should not merge it yet.

javierdiaz72 · 2025-01-23T19:06:56Z

Hi, @geo2a! Do you have an idea why some of the CI checks are still failing?

amesgen · 2025-01-23T19:42:47Z

CI is complaining about the fact that some files don't have LF (unix style) line endings: https://ci.iog.io/build/6541916/nixlog/1 (also see #1253/#1252).
Concretely, the file in question is docs/agda-spec/src/Spec/hs-src/test/OperationalCertificateSpec.hs. Maybe this is something you could configure in your editor?

javierdiaz72 · 2025-01-23T21:26:09Z

CI is complaining about the fact that some files don't have LF (unix style) line endings: https://ci.iog.io/build/6541916/nixlog/1 (also see #1253/#1252). Concretely, the file in question is docs/agda-spec/src/Spec/hs-src/test/OperationalCertificateSpec.hs. Maybe this is something you could configure in your editor?

Thanks for pointing that out, Alex! I've just fixed the issue with the file and now the CI is not complaining anymore. 🙂

javierdiaz72 · 2025-02-14T19:51:02Z

Hey, folks! I'm not sure why the last CI check is failing. Could anybody help me out?

geo2a · 2025-02-17T13:29:48Z

@javierdiaz72 it seems like the failure was transient, I've re-triggered the job and the failure went away.

geo2a · 2025-02-18T11:32:45Z

Thanks @javierdiaz72 for this monumental work!

Before we merge this, we need to work a little more on documentation and Git history:

Could you please write a README.md for the docs/agda-spec directory? I think it should include:
- the outline structure of the project: what Haskell code is static, what is generated and a could of words on how the two are tied together
- instructions on how to generate, build and test the Haskell code, assuming that we are in the Nix shell, i.e. nix develop .#agda-spec
Once the above is done, could you also create a small section in the top-level README.md that references docs/agda-spec/README.md
Finally, could you rebase on top of current main and squash all commits into one, keeping the rough sequence in the commit message?

Please let me know if you need any help with these!

Another question:

Do we still need the files in docs/agda-spec/nix? I do think they are used anywhere.

Otherwise the PR looks great! I have verified that the Haskell code is generated, build and tested with:

nix build .#agda-spec.hsExe --rebuild --print-build-logs 2>&1 | tee tmp.log

the test results should be somewhere near the end of the output.

geo2a · 2025-02-18T14:25:57Z

@javierdiaz72 another request I got form the team is to provide instructions to build the spec and run the tests without Nix. How hard would that be? Would it be possible for you to outline in the README what additional steps one needs to follow besides the Agda installation instructions?

geo2a · 2025-02-18T14:33:10Z

docs/agda-spec/src/Spec/hs-src/cardano-consensus-executable-spec.cabal

+        base >=4.14 && <4.21,
+        text,
+        ieee
+-- This will be generated automatically when building with nix


When building the source derivation with Nix, e.g. nix build .#agda-spec.hsSrc, this section is indeed filled in with a long list of module names. @javierdiaz72 do you know exactly what bit of code is responsible for this? Is this a blocker for providing a non-Nix build option?

The code responsible for that is:

ouroboros-consensus/docs/agda-spec/src/Makefile

Lines 44 to 46 in 5ba7a4a

find $(HS_DIST)/MAlonzo -name "*.hs" -print\

| sed "s#^$(HS_DIST)/# #;s#\.hs##;s#/#.#g"\

>> $(HS_DIST)/$(CABAL_FILE)

Therefore, it's not related to Nix.

Generate Haskell code for TickNonce

4a4a962

javierdiaz72 added enhancement New feature or request formal-spec Changes related to formal specifications conformance Changes related to conformance testing labels Nov 21, 2024

javierdiaz72 self-assigned this Nov 21, 2024

Fix Cabal version in Cabal file

1333e69

javierdiaz72 added 2 commits December 5, 2024 19:25

Complete support for dummy constants and cryptography

7a8846b

Generate Haskell code for UpdateNonce

9302544

geo2a mentioned this pull request Dec 12, 2024

Integrate the Haskell code generate from agda-spec into the build system and CI #1343

Open

3 tasks

javierdiaz72 force-pushed the javierdiaz72/agda-spec-to-haskell branch 3 times, most recently from 43c9f54 to f3361a3 Compare December 12, 2024 19:07

Remove unnecessary parameters from PParams

a98ba32

Signed-off-by: Javier Díaz <[email protected]>

javierdiaz72 force-pushed the javierdiaz72/agda-spec-to-haskell branch from f3361a3 to a98ba32 Compare December 12, 2024 19:14

javierdiaz72 and others added 2 commits December 12, 2024 20:22

Relocate ExternalStructures

fdee730

Use GHC that comes with Agda and expose it in the shell

4e65a0e

geo2a mentioned this pull request Dec 13, 2024

Integrate the Haskell code emitted from agda-spec into CI #1344

Merged

geo2a added 2 commits December 13, 2024 12:35

Emit, build and test the Haskell code from agda-spec

a9e2699

geo2a linked an issue Dec 16, 2024 that may be closed by this pull request

Integrate the Haskell code generate from agda-spec into the build system and CI #1343

Open

3 tasks

Merge remote-tracking branch 'refs/remotes/origin/javierdiaz72/agda-s…

a482527

…pec-to-haskell' into javierdiaz72/agda-spec-to-haskell

Add support for code auto-generation of records with non-dependent fu…

5dc3eeb

…nction fields

geo2a force-pushed the javierdiaz72/agda-spec-to-haskell branch 2 times, most recently from b307ad4 to 5987184 Compare December 18, 2024 10:41

Fix formatting/linting

f2af22c

- dos2unix - hlint - make `cardano-consensus-executable-spec.cabal` pass `cabal.check` Make `cardano-consensus-executable-spec.cabal` pass `cabal.check` Copy licence files instead of linking fix cabal file

geo2a force-pushed the javierdiaz72/agda-spec-to-haskell branch from 5987184 to f2af22c Compare December 18, 2024 11:22

Generate Haskell code for OperationalCertificate

15b0b19

Convert OperationalCertificateSpec.hs to Unix format

461b989

javierdiaz72 added 3 commits February 7, 2025 17:22

Generate Haskell code for Protocol

868ecb4

Generate Haskell code for TickForecast

a872e1f

Generate Haskell code for ChainHead

5ba7a4a

javierdiaz72 marked this pull request as ready for review February 17, 2025 14:13

javierdiaz72 requested review from nfrisby, jasagredo, amesgen, fraser-iohk, dnadales and geo2a as code owners February 17, 2025 14:13

geo2a reviewed Feb 18, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Generate Haskell code from the Agda spec #1315

Generate Haskell code from the Agda spec #1315

javierdiaz72 commented Nov 21, 2024 •

edited by geo2a

Loading

javierdiaz72 commented Nov 21, 2024

abailly commented Nov 25, 2024

amesgen commented Nov 25, 2024

abailly commented Nov 25, 2024

abailly commented Nov 25, 2024

amesgen commented Nov 25, 2024

abailly commented Nov 25, 2024

amesgen commented Nov 25, 2024

abailly commented Nov 25, 2024

geo2a commented Jan 13, 2025

javierdiaz72 commented Jan 20, 2025

javierdiaz72 commented Jan 23, 2025 •

edited

Loading

amesgen commented Jan 23, 2025

javierdiaz72 commented Jan 23, 2025

javierdiaz72 commented Feb 14, 2025

geo2a commented Feb 17, 2025

geo2a commented Feb 18, 2025 •

edited

Loading

geo2a commented Feb 18, 2025 •

edited

Loading

geo2a Feb 18, 2025

javierdiaz72 Feb 20, 2025

	find $(HS_DIST)/MAlonzo -name "*.hs" -print\
	\| sed "s#^$(HS_DIST)/# #;s#\.hs##;s#/#.#g"\
	>> $(HS_DIST)/$(CABAL_FILE)

Generate Haskell code from the Agda spec #1315

Are you sure you want to change the base?

Generate Haskell code from the Agda spec #1315

Conversation

javierdiaz72 commented Nov 21, 2024 • edited by geo2a Loading

javierdiaz72 commented Nov 21, 2024

abailly commented Nov 25, 2024

amesgen commented Nov 25, 2024

abailly commented Nov 25, 2024

abailly commented Nov 25, 2024

amesgen commented Nov 25, 2024

abailly commented Nov 25, 2024

amesgen commented Nov 25, 2024

abailly commented Nov 25, 2024

geo2a commented Jan 13, 2025

javierdiaz72 commented Jan 20, 2025

javierdiaz72 commented Jan 23, 2025 • edited Loading

amesgen commented Jan 23, 2025

javierdiaz72 commented Jan 23, 2025

javierdiaz72 commented Feb 14, 2025

geo2a commented Feb 17, 2025

geo2a commented Feb 18, 2025 • edited Loading

geo2a commented Feb 18, 2025 • edited Loading

geo2a Feb 18, 2025

Choose a reason for hiding this comment

javierdiaz72 Feb 20, 2025

Choose a reason for hiding this comment

javierdiaz72 commented Nov 21, 2024 •

edited by geo2a

Loading

javierdiaz72 commented Jan 23, 2025 •

edited

Loading

geo2a commented Feb 18, 2025 •

edited

Loading

geo2a commented Feb 18, 2025 •

edited

Loading