Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Agda html #5827

Merged
merged 6 commits into from
Mar 13, 2024
Merged

Agda html #5827

merged 6 commits into from
Mar 13, 2024

Conversation

ramsay-t
Copy link
Contributor

This is a small PR to convert all of the metatheory files to Markdown - specifically, everything should now be .lagda.md and should be Markdown style Literate Agda. The files have consistent Markdown style code blocks and headings, but not a huge amount of actual text yet.

The command nix build ".#plutus-metatheory-site" should convert the Agda code to HTML and then the markdown to HTML, resulting in a set of linked and formatted HTML documents. The auto-generated CSS is pretty basic, so this could be augmented before this gets integrated with a release process? The current script uses Jekyll but I have a working Pandoc based bash script if that is preferred.

@ramsay-t ramsay-t requested review from zliu41 and joseph-fajen March 11, 2024 13:33
@ramsay-t ramsay-t added the No Changelog Required Add this to skip the Changelog Check label Mar 11, 2024
@michaelpj
Copy link
Contributor

The build of the metatheory Haskell package (cabal build plutus-metatheory) is broken. I suspect it's this line: https://github.com/IntersectMBO/plutus/blob/master/plutus-metatheory/Setup.hs#L81, the suffix needs to change.

@ramsay-t ramsay-t self-assigned this Mar 11, 2024
@michaelpj
Copy link
Contributor

Did you try it? It still doesn't work and I'm not sure why. It doesn't seem to be running the preprocessor at all for some reason.

@michaelpj
Copy link
Contributor

Ping @zeme-wana . I've tried various options for the preprocessor extension and it just mysteriously seems to never trigger? I'm very unsure what's going on here.

@ramsay-t
Copy link
Contributor Author

Did you try it? It still doesn't work and I'm not sure why. It doesn't seem to be running the preprocessor at all for some reason.

You were right about the extension, but it now builds fine in nix on my mac... These hydra test builds all seem to just not bother with the preprocessor - it is producing dozens of errors, each of which is "Can't find file: " and then a MAlonzo file that should be built by the preprocessor.

@michaelpj
Copy link
Contributor

You were right about the extension, but it now builds fine in nix on my mac... These hydra test builds all seem to just not bother with the preprocessor - it is producing dozens of errors, each of which is "Can't find file: " and then a MAlonzo file that should be built by the preprocessor.

Yes, the preprocessor is not running. I think you may find it doesn't work if you cabal clean first, you probably just have cached versions of the MAlonzo files.

@michaelpj michaelpj merged commit 4cb1d64 into IntersectMBO:master Mar 13, 2024
7 checks passed
Unisay added a commit that referenced this pull request Mar 18, 2024
@Unisay @kwxm
@ramsay-t @dependabot
CIP-0057: Alternative approach to deriving and referencing schema def…
5526150 
…initons. (#5839)

* Add pointer to issue on the ledger's cost model interface (#5828)

* Agda html (#5827)

* Moved all Agda files to Markdown.

* Added some brief text to the TOC

* Fixed the file extension in Setup.hs for the Markdown Agda.

* Added all possible file extensions and the preprocessor seems to run now.

* Cleaned out .lagda from the cabal file, since everything is .lagda.md now.

* chore(deps): bump tj-actions/changed-files from 42 to 43 (#5835)

Bumps [tj-actions/changed-files](https://github.com/tj-actions/changed-files) from 42 to 43.
- [Release notes](https://github.com/tj-actions/changed-files/releases)
- [Changelog](https://github.com/tj-actions/changed-files/blob/main/HISTORY.md)
- [Commits](tj-actions/changed-files@v42...v43)

---
updated-dependencies:
- dependency-name: tj-actions/changed-files
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <[email protected]>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

* Kwxm/correct conformance comments (#5829)

* Fix comments in conformance tests

* Fix comments in conformance tests

* Fix comments in conformance tests

* CIP-57: unroll top level types

* Extract `goldenJson` function and move it to the `Tests.Lib`

* Note about unrolling types

* CIP-57: accumulate schema definitions preserving types for safe refs.

* Build schema definitions by un-rolling a list of top-level types.

* validatorParameters :: []

---------

Signed-off-by: dependabot[bot] <[email protected]>
Co-authored-by: Kenneth MacKenzie <[email protected]>
Co-authored-by: Ramsay Taylor <[email protected]>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Unisay added a commit that referenced this pull request Mar 18, 2024
@Unisay @kwxm
@ramsay-t @dependabot
CIP-0057: Alternative approach to deriving and referencing schema def…
b78aee0 
…initons. (#5839)

* Add pointer to issue on the ledger's cost model interface (#5828)

* Agda html (#5827)

* Moved all Agda files to Markdown.

* Added some brief text to the TOC

* Fixed the file extension in Setup.hs for the Markdown Agda.

* Added all possible file extensions and the preprocessor seems to run now.

* Cleaned out .lagda from the cabal file, since everything is .lagda.md now.

* chore(deps): bump tj-actions/changed-files from 42 to 43 (#5835)

Bumps [tj-actions/changed-files](https://github.com/tj-actions/changed-files) from 42 to 43.
- [Release notes](https://github.com/tj-actions/changed-files/releases)
- [Changelog](https://github.com/tj-actions/changed-files/blob/main/HISTORY.md)
- [Commits](tj-actions/changed-files@v42...v43)

---
updated-dependencies:
- dependency-name: tj-actions/changed-files
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <[email protected]>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

* Kwxm/correct conformance comments (#5829)

* Fix comments in conformance tests

* Fix comments in conformance tests

* Fix comments in conformance tests

* CIP-57: unroll top level types

* Extract `goldenJson` function and move it to the `Tests.Lib`

* Note about unrolling types

* CIP-57: accumulate schema definitions preserving types for safe refs.

* Build schema definitions by un-rolling a list of top-level types.

* validatorParameters :: []

---------

Signed-off-by: dependabot[bot] <[email protected]>
Co-authored-by: Kenneth MacKenzie <[email protected]>
Co-authored-by: Ramsay Taylor <[email protected]>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
v0d1ch pushed a commit to v0d1ch/plutus that referenced this pull request Dec 6, 2024
@ramsay-t @v0d1ch
Agda html (IntersectMBO#5827)
6e96a7b 
* Moved all Agda files to Markdown.

* Added some brief text to the TOC

* Fixed the file extension in Setup.hs for the Markdown Agda.

* Added all possible file extensions and the preprocessor seems to run now.

* Cleaned out .lagda from the cabal file, since everything is .lagda.md now.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@michaelpj michaelpj michaelpj approved these changes

@zliu41 zliu41 Awaiting requested review from zliu41

@joseph-fajen joseph-fajen Awaiting requested review from joseph-fajen

Assignees

@ramsay-t ramsay-t

Labels
No Changelog Required Add this to skip the Changelog Check
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@ramsay-t @michaelpj