Théo Zimmermann

Yes, it is also my understanding that you can combine files under LGPL 2.1 and files under GPL 3+ and the overall thing is GPL 3+.

This is a SerAPI issue, worth reporting upstream. It can be reproduced within sertop with: ```lisp (Add () "From mathcomp Require Import all_ssreflect.") (Add () "From HB Require Import structures.")...

>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...

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...

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.

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...

> 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...

> 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...

> I think this is already possible, actually :) Navigating to the point where you want the lemma extracted and pressing C-c C-a C-x will insert the lemma where the...

I'm especially interested in support for `pass` since this is the password manager I use. Generally speaking, integration with command-line password managers should be quite doable.