Generate Haskell code from the Agda spec

[javierdiaz72]

This PR resolves #1312 and #1343.

[javierdiaz72]

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]

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]

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]

@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]

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]

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]

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

[amesgen]

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]

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