8000 New literate programming backend forester, `*.lagda.tree` by dannypsnl · Pull Request #7403 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

New literate programming backend forester, *.lagda.tree #7403

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
Merged
merged 9 commits into from
Oct 10, 2024
Merged

New literate programming backend forester, *.lagda.tree #7403

merged 9 commits into from
Oct 10, 2024

Conversation

dannypsnl
Copy link
Contributor

forester is a tool to manage forests of evergreen notes, each note is a file with suffix .tree.

Here I propose a basic support to treat files *.lagda.tree as a literate programming sources, follow structure of others literate languages, hope the format is proper.

andreasabel
andreasabel reviewed Oct 9, 2024
View reviewed changes
andreasabel
andreasabel reviewed Oct 9, 2024
View reviewed changes
@andreasabel
Copy link
Member

@dannypsnl Sorry for the late review.

LGTM.
Would need a CHANGELOG and user-manual entry.

@andreasabel andreasabel added this to the 2.8.0 milestone Oct 9, 2024
@dannypsnl
New literate programming backend forester, *.lagda.tree
ed3340f 
Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
@dannypsnl
Fix test
c0293c8 
Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
@dannypsnl
Provide test cases
ee49ab1 
Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
@dannypsnl
follows the review suggestions
d57661a 
Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
@dannypsnl
doc: add literate forester entry in user manual
530b1c7 
Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
@dannypsnl
Copy link
Contributor Author

I follow the suggestions & add new entry into user manual, but I'm not sure where should I put the text in CHANGELOG.md.

@dannypsnl
to fix build failed
eb8dc72 
Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
@dannypsnl
missing open braces
278a063 
Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
@dannypsnl
fix rst
40b8eaf 
Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
@andreasabel
Copy link
Member

I follow the suggestions & add new entry into user manual,

Thanks!

but I'm not sure where should I put the text in CHANGELOG.md.

Dunno, does not fit under the existing rubric.
Maybe just first in section Syntax.

@dannypsnl
update CHANGELOG
c1d7cca 
Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
@dannypsnl
Copy link
Contributor Author

The rst build failed in CI, though I run make html is fine in local nix develop environment.

@andreasabel
Copy link
Member
andreasabel commented Oct 10, 2024 •
edited
Loading

The rst build failed in CI, though I run make html is fine in local nix develop environment.

Runs fine for me as well, locally.
Could be that we are not Sphinx-8 compatible, but the CI is using it: https://github.com/agda/agda/actions/runs/11269145770/job/31337190029?pr=7403#step:7:18

Running Sphinx v8.0.2
WARNING: Calling get_html_theme_path is deprecated. If you are calling it to define html_theme_path, you are safe to remove that code.

@andreasabel andreasabel added the pr: squash-me This PR needs squashing label Oct 10, 2024
@andreasabel
Copy link
Member

Thanks!

@andreasabel andreasabel merged commit 628f6d1 into agda:master Oct 10, 2024
27 of 28 checks passed
@andreasabel andreasabel self-assigned this Oct 10, 2024
@dannypsnl dannypsnl deleted the literate-forester branch October 10, 2024 12:32
@dannypsnl dannypsnl mentioned this pull request Oct 10, 2024
Closed
@andreasabel
Copy link
Member

WARNING: Calling get_html_theme_path is deprecated. If you are calling it to define html_theme_path, you are safe to remove that code.

Fixed by

fredins pushed a commit to fredins/agda that referenced this pull request Nov 24, 2024
@dannypsnl @fredins
New literate programming backend forester, *.lagda.tree (agda#7403)
07cf1d1 
* New literate programming backend forester, `*.lagda.tree`

Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>

* Fix test

Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>

* Provide test cases

Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>

* follows the review suggestions

Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>

* doc: add literate forester entry in user manual

Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>

* to fix build failed

Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>

* missing open braces

Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>

* fix rst

Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>

* update CHANGELOG

Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>

---------

Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
Authored-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
andreasabel added a commit that referenced this pull request Jan 19, 2025
@andreasabel
Fixup #7403 tests: add missing golden values
f4c3c39 
PR #7403 was incomplete as it did not add the new extension
.lagda.tree to the test runner, so, the tests were actually not run.
@andreasabel andreasabel mentioned this pull request Jan 19, 2025
Merged
@liamoc
Copy link
Contributor
liamoc commented May 14, 2025

Am I missing something? This doesn't generate valid tree files, it generates HTML files with some forester notation left in there.

@dannypsnl
Copy link
Contributor Author

@liamoc Indeed, my original plan is using external tool to continue turn left files to valid tree files, but if you prefer, I can try to modify agda itself to complete this job.

@andreasabel andreasabel mentioned this pull request May 14, 2025
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@andreasabel andreasabel andreasabel approved these changes

Assignees

@andreasabel andreasabel

Labels
literate-agda pr: squash-me This PR needs squashing
Projects
None yet
Milestone
2.8.0
Development

Successfully merging this pull request may close these issues.
3 participants
@dannypsnl @andreasabel @liamoc
0