search

wenkokke / agda2html

a tool to convert literate agda to html
GNU Lesser General Public License v3.0
6 stars 1 forks source link

Using other agda libraries #1

Open jonaprieto opened 6 years ago

jonaprieto commented 6 years ago

Hi Wen,

I found helpful this program. I was wondering what about to make the name of the library as a parameter to support listings of other agda libraries available on Github.

I was thinking in something like this:

agda2html --verbose --github-user=agda --library=agda-stdlib --jekyll-root=out/ -i $< -o $@

Best,

Jonathan.

wenkokke commented 6 years ago

I was thinking of some rewrite along these lines, yeah, using the Agda module system. For the Agda standard library you'd unfortunately need to set a whopping three parameters, as you'd need to set the GitHub user, the repository name, and the library name (which is standard-library). This way I could also stop downloading the repository if it's available locally.

wenkokke commented 6 years ago

Another objection is that having a GitHub repository doesn't necessarily tell you if and where clickable HTML is available. Therefore, I'd prefer some complex series of options, where you can give a GitHub repository as agda/agda-stdlib or a library name (if it's available locally) and optionally a URL template, as in https://agda.github.io/agda-stdlib/%s.html...