search

dannypsnl / agda-tree

literate programming agda in forester
https://crates.io/crates/agda-tree
GNU General Public License v3.0
2 stars 0 forks source link

literate programming #3

Open dannypsnl opened 3 months ago

dannypsnl commented 3 months ago

Once most things are done, back port to let agda ignore non-program part in *.lagda.tree.

dannypsnl commented 3 months ago

draft: https://github.com/dannypsnl/agda/commit/81a63edab24b38afa2278610b930908e25285d25

dannypsnl commented 3 months ago

Agda treats literate programming by ignore source language's semantic and extract only code block, then generates HTML like below

<pre class="Agda"><a id="1" class="Background"># coproduct

&lt;details&gt;&lt;summary&gt;Helpers&lt;/summary&gt;

</a><a id="51" class="Markup">```agda
</a><a id="59" class="Keyword">module</a> <a id="66" href="coproduct.html" class="Module">coproduct</a> <a id="76" class="Keyword">where</a>
<a id="82" class="Keyword">open</a> <a id="87" class="Keyword">import</a> <a id="94" href="foundation.html" class="Module">foundation</a>

as we can see, the original markdown are put into class="Background". I expect the modification I'm doing will lead to similar situation.

dannypsnl commented 3 months ago

At this workflow, we can expect that index.agda is managed by users themself, so invoke agda --html ... is not the job of agda-tree anymore, instead, it simply combine *.lagda.tree with html/*.html to get *.tree.

dannypsnl commented 3 weeks ago

Since the PR https://github.com/agda/agda/pull/7403 is merged, 2.8.0 will have new literate backend, the new workflow is replacing generated html with forester html namespace syntax.