Feature Request: Github actions

[Bruno-366]

Hello! Love the project, is there any way to use alectryon as a github action? For example to publish it to Github Pages? The README mentions that it could integrate with Sphinx, Docutils, Pelican, readthedocs, Nikola. Is that the recommended approach?

I'm pretty sure github actions usually use docker, and I could create a dockerfile that essentially does the following

find . -name *.v -exec alectryon.py --frontend coq+rst --backend webpage {} \;

[Zimmi48]

I'm pretty sure github actions usually use docker

That's one way, but not the only one.

Anyway, are you aware of https://github.com/coq-community/docker-coq-action? If the Docker-Coq images (https://github.com/coq-community/docker-coq) were extended to include Alectryon, then it would be easy to add the command you mention as one of the custom steps.

[Bruno-366]

Hmm... the docker-coq action readme wasn't too helpful, but the docker-coq wiki mentions that:

it is possible to install additional APT [...] packages using sudo apt-get

So if we could package alectryon that would be great, since there doesn't seem to be a package for APT. (nor for AUR, which was a surprise).

...Ah, ok so: the docker-coq wiki linked to a docker-coq action demo which seems to be for building coq projects.

---

The docker-coq action README mentions an .opam file, and I suppose this is because opam is the package manager for ocaml and coq is built on top of ocaml? yep, seems so.

Ok, so the docker-coq action README also mentions a custom_script and some bash snippets, that can be modified corresponding to:

• before installation,
• during installation,
• and after installation
• ({{before_install}} {{install}} {{after_install}})

So I suppose what you meant is altering one of these to include Alectryon. Problem is, it doesn't seem like Alectryon is being packaged by opam either. So perhaps that should be a first step?

[Bruno-366]

Or perhaps since alectryon is written in python it would make most sense to build an APT package (ie alectryon.deb) rather than an opam one? Note to self, see: alectryon/etc/vm/provision.sh

[Zimmi48]

My suggestion was even to go further than this and request the inclusion of Alectryon in the standard Docker-Coq images. If this was done, then there would be no need to install it during the call to Docker-Coq-Action, it would just need to be called during one of those custom steps that you identified.

[Bruno-366]

Ok, thank you :) So docker-coq is the "standard" one? I'll give them a heads up.

I was a bit confused with the structure of everything, but it seems like its: docker-coq-action (GitHub action) --> docker-qoc (Dockerfile) --> docker-base (Dockerfile still from coq-community) --> debian docker and the demo is not really a dockerfile or github action meant to be used, so much as a repo using docker-coq-action as a demonstration. and all the before/after install/script in docker-qoc-action README were actually just pure bash written really un-idiomatically (as the startGroup and endGroup were just bash functions, defined here) and docker-qoc-action does docker-qoc, only that its actually named coqorg/coq on dockerhub

[Bruno-366]

although thinking about it, creating a .deb or pip package still seems like a good idea, not just for the end user who wants to use and install alectryon, but also so that docker-coq can include it using apt-get rather than by cloning the repo, which just seems messy.

creating a pip package uploading a pip package

[Zimmi48]

BTW, @Bruno-366, if you see how to improve things with respect to the documentation of Docker-Coq / Docker-Coq-Action, feel free to open PRs.

[Bruno-366]

I half-laugh since I'm still not 100% sure I'm correct, but with that said, I that the problem for me was mainly that everything is split into many interrelated projects. The information is there, but its hard to see since its a lot of context that is needed. I'll try to make PR, see how things go.

[Zimmi48]

What you wrote in https://github.com/cpitclaudel/alectryon/issues/39#issuecomment-832865282 is fully correct (apart from the spelling of coq into qoc :laughing:).

I that the problem for me was mainly that everything is split into many interrelated projects.

Yeah, maybe adding more links and explaining the relationships would help.

[cpitclaudel]

HI Bruno, I think adding Alectryon to docker-coq would be wonderful 👍 Let me know if you run into issues. I think a .deb package will take a long time to propagate if we want it in official sources, so it would likely be best to just clone the repo or make either an OPAM package, or a pypi package.

[Zimmi48]

HI Bruno, I think adding Alectryon to docker-coq would be wonderful :+1: Let me know if you run into issues.

Let's cc @erikmd here (although this would warrant a proper issue on the docker-coq repo).

[erikmd]

Hi @Bruno-366 (thanks @Zimmi48 thanks for the Cc!)

I actually thought recently about a similar idea 🙂 (extending docker-coq-action or so with Alectryon support) when preparing this term a course of Coq with some deployment to GitHub Pages − here is the link FTR: https://github.com/pfitaxel/tapfa-coq-alectryon#readme https://github.com/pfitaxel/tapfa-coq-alectryon/blob/master/.github/workflows/deploy.yml

but I wasn't sure @Zimmi48 and @cpitclaudel precisely would be OK to extend docker-coq and/or docker-coq-action in a similar way to automate this "officially", but given this issue you just opened, I guess I have some answer 😊

With a bit of chance, maybe I'll have the time to prepare some PoC regarding this automation, by next WE (May 16th). So I will open an issue in docker-coq-action to keep track of this − but in the meantime for your own GitHub repo, you may want to directly draw some inspiration from the deploy.yml file above.

However, note that the addition of Alectryon to Docker-Coq can't be done trivially for each version of Coq (in a uniform way, I mean) because:

• Alectryon depends on serapi (Clément, do you know what is the earliest compatible version of coq-serapi?)
• coq-serapi requires Coq ≥ 8.7 anyway
• while Docker-Coq images are supported from each major release of Coq ≥ 8.4 (details)

[Bruno-366]

Ok that's cool then 😄 I started a repo for the github action where I was trying to figure out how to make things work 😅 , but I suppose if alectryon is included in docker-coq-action, then that would seem like a sane default that most people could rely on automatically.

[erikmd]

Hi @Bruno-366, indeed; but as I just said in my previous comment (after the edit), you can use, from now on, this complete GHA workflow as a template for your needs: https://github.com/pfitaxel/tapfa-coq-alectryon/blob/master/.github/workflows/deploy.yml

[Bruno-366]

oh ok cool :) I'll try it out

[cpitclaudel]

Hi @erikmd , I'm not 100% sure what the oldest supported version is. I think 8.10.0+0.7.0.

[erikmd]

OK!

BTW regarding your earlier comment, @cpitclaudel:

I think a .deb package will take a long time to propagate if we want it in official sources, so it would likely be best to just clone the repo or make either an OPAM package, or a pypi package.

do you think it's easy to setup an .opam package specification for alectryon itself? (I'm not 100% sure it's feasible for the python part though, so maybe a few conf-* packages would be needed? or more hacks?)

Because in this case, installing Alectryon would be as easy as doing:

opam pin add alectryon "https://github.com/cpitclaudel/alectryon.git#master"

Otherwise, if you think it's not feasible to easily combine the python+ocaml parts in a single OPAM package, do you believe one could advise running first the opam command above, then either one of the following two pip commands?

pip install git+https://github.com/cpitclaudel/alectryon.git@master
pip install https://github.com/cpitclaudel/alectryon/archive/master.zip

(according to https://stackoverflow.com/a/24811490/9164010, the second command might be faster)

[cpitclaudel]

Alectryon doesn't have any OCaml code — it's all Python. So a pip package would likely make a lot of sense, I just haven't investigated how one would do that :) I think it would be quite reasonable to tell people to install SerAPI and Coq with opam and then Alectryon with pip.

[erikmd]

OK! thank you @cpitclaudel for your feedback; for the record, there are several pip packages that already work in this way (I mean, not everything is installed by pip, only the "frontend" part or so) − e.g., https://pypi.org/project/docker-compose/

[cpitclaudel]

Thanks @erikmd ! I hope someone will have time to prepare such a package, then :)

[Zimmi48]

I hope someone will have time to prepare such a package, then :)

Maybe you should open a separate issue dedicated to the question of a PyPI package and label it as "help wanted".

[cpitclaudel]

Good point, done (#41)

[cpitclaudel]

Update @erikmd: there's a PyPI package for alectryon now (pip install alectryon)