Emilio Jesús Gallego Arias (Nov 12 2018 at 18:21): Emilio Jesús Gallego Arias (Nov 12 2018 at 18:21):Salut tout le monde, paramcoq has been added to Coq's CI :)
Théo Zimmermann (Nov 13 2018 at 18:03):Hey @Emilio Jesús Gallego Arias! You are the first one to use this chat room. Welcome!
Emilio Jesús Gallego Arias (Nov 13 2018 at 18:45):Salut @Théo Zimmermann , merci !
Emilio Jesús Gallego Arias (Nov 13 2018 at 18:45)::D
Emilio Jesús Gallego Arias (Nov 13 2018 at 18:45):This seems like a good place to chat with plugin authors who are not coq devs
Théo Zimmermann (Nov 13 2018 at 19:04):Indeed, it could be. Feel free to tell people to come here.
Karl Palmskog (Nov 15 2018 at 01:44):will coqpp be mandatory for plugins in 8.10, or will ml4 still work?
Karl Palmskog (Nov 15 2018 at 01:59):oh, and if plugin advice is on the table: is it possible at all to use native code in a Coq plugin? I tried to call C code through OCaml but could never get it to compile.
Emilio Jesús Gallego Arias (Nov 15 2018 at 04:41):Hi @Karl Palmskog , ml4 will likely not supported in 8.10
Emilio Jesús Gallego Arias (Nov 15 2018 at 04:41):There should not be a problem to use C code from a plugin, however I do recommend you use the Dune build system to do that
Emilio Jesús Gallego Arias (Nov 15 2018 at 05:15):Here is a proof of concept https://github.com/ejgallego/coq-cplugin
Karl Palmskog (Nov 15 2018 at 14:49):@Emilio Jesús Gallego Arias thanks, that's just what I've been looking for
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:04):No prob
Karl Palmskog (Nov 15 2018 at 15:06):@Emilio Jesús Gallego Arias do you recommend switching any Coq-related projects that use OCaml to Dune? We have a quite a few that use OCamlbuild
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:06):for extra fun with that build setup synlink your current coq master folder to the plugin root folder and you will see how the plugin composes with Coq itself
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:06):@Karl Palmskog not yet
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:06):I recommend developing the ML parts with Dune tho
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:07):coq_dune needs a few tweaks so it can produce rules for vo building, right now it is only used to build the stdlib
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:07):but once we get the vo bussiness sorted out I do believe using Dune will provide a much better experience
Karl Palmskog (Nov 15 2018 at 15:07):OK, so basically we should stick with Make for overall building, but swap out OCamlbuild for the OCaml parts?
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:08):if what you mean is moving from Ocamlbuild -> Dune I'd say you will get quite a few benefits
Karl Palmskog (Nov 15 2018 at 15:08):OK sounds good
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:08):Coq master if fully dunerized so if you switch to Dune you get a composed build and that's very pleasant to use
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:08):in general
Karl Palmskog (Nov 15 2018 at 15:09):we tend to only target the released Coq versions though
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:09):you can do that too, but you won't a composed build
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:09):for me the composed build is essential as I tend to develop on a plugin / toplevel and Coq at the same time, so my rebuilds are blazing fast
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:10):in fact it is strange that some Coq devs still keep using Make for Coq itself as dune build @check outperforms make by a large amount
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:10):but in general most OCamlbuild setups will only get improvements from switching to dune
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:10):YMMV
Karl Palmskog (Nov 15 2018 at 15:11):so the plan is to throw out coq_makefile eventually?
Karl Palmskog (Nov 15 2018 at 15:11):and everybody does coq_dune?
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:12):I guess so, maybe coq_makefile stays for a while, it is not incompatible with Dune
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:12):but indeed coq_dune will provide more features, for example a notion of package
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:12):so you can finally say in your Coq project "I depend on stdlib.streams"
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:12):instead of having to mess with flags
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:13):and will also support composition which in the Dune world means
Take n repositories that use dune, arrange them in any way on the file system and the result is still a single repository that dune knows how to build at once.
Karl Palmskog (Nov 15 2018 at 15:14):and it will ignore library boundaries, so I won't build the whole ssreflect if I only depend on bigop or something like that?
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:16):indeed
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:16):that's _so_ convenient
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:16):when composing a new global set of rules is created
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:17):so that's a blessing when working with plugins and modifying Coq for example, I don't need to wait
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:17):it also uses OCaml -opaque which means a big practical speedup, etc...
Karl Palmskog (Nov 15 2018 at 15:20):since I don't hack Coq often, the only real pain I've had is with extracted OCaml files... they have to be manually specified in something like Make, but I guess Dune has similar features
Karl Palmskog (Nov 15 2018 at 15:20):for example, we often only want to build the OCaml project without checking all the proofs
Karl Palmskog (Nov 15 2018 at 15:20):or do just-enough-proof-checking-to-get-extracted-file
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:26):we could indeed have better support for extracted files, you can add rules in Dune for them
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:26):that's a good idea to add to the coq_dune file, a field indicating which libraries are extracted
Karl Palmskog (Nov 15 2018 at 15:35):distributed systems verification projects have this absurd ratio of proofs-to-code
Karl Palmskog (Nov 15 2018 at 15:35):maybe 20:1 or more in my experience
Karl Palmskog (Nov 15 2018 at 15:36):code gets extracted in 20 seconds, proofs take 1h to check
Karl Palmskog (Nov 15 2018 at 15:36):at least they're not tightly coupled
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:43):you are talking about verdi?
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:43):and verdi-raft?
Karl Palmskog (Nov 15 2018 at 15:43):for example, we're working on new projects
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:43):similar ratios have been found in other project like for example the verified lucid compiler
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:43):it is funny as we are discussing verdi and verdi-raft in our distributed system verif seminar in Paris :)
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:45):indeed one question we had is how to improve the ratio there, and how to make statements of theorems a bit more legible
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:45):we were discussing some tricks used in math-comp in fact :)
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:46):proof checking is indeed a pain in coq, some "hacks" such as vos/vok [see PR] should help and will be supported by coq_duen
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:46):I also wanted to write you about incremental compilation
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:46):but the thing is that Coq cannot currently process proofs properly in parallel and indeed it is looking like it won't be able to do so for a while :/
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:47):I wrote some time ago a prototype of a new scheduler that could help a bit, however, it is killed by sections
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:47):and I don't know how to solve that problem; Proof Using is not a solution to me
Karl Palmskog (Nov 15 2018 at 15:55):I think in big projects Proof using. is feasible, we were able to automate annotations
Karl Palmskog (Nov 15 2018 at 15:56):basically, one can run auto-annotate once a week or something
Karl Palmskog (Nov 15 2018 at 15:57):anyway, even selection/parallelism at the file level can help a lot
Karl Palmskog (Nov 15 2018 at 15:57):and then tricks like using a 32-bit Coq (we get 20% speedup or so)
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:58):flambda can get you another 10% easily
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:58):with the right options, as documented on INSTALL
Karl Palmskog (Nov 15 2018 at 15:58):oh, good to know
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:58):yup it is ridiculous how faster 32bits are
Karl Palmskog (Nov 15 2018 at 15:59):sadly these tricks don't seem to be widely known
Emilio Jesús Gallego Arias (Nov 15 2018 at 15:59):well it is documented in install and we have insisted a bit on it; but yeah, it is hard to get people to use it; at least the default binary builds will be optimized
Emilio Jesús Gallego Arias (Nov 15 2018 at 16:00):I dislike Proof using tho, it is really cumbersome, and the user should just not be aware of that. I can imagine situations where the context is like in the hundredths of section variables, so Coq should take care of that; unfortunately that's a hard problem to solve.
Emilio Jesús Gallego Arias (Nov 15 2018 at 16:01):Maybe if we add incremental support to .vo files we could indeed handle Proof using like info automatically
Emilio Jesús Gallego Arias (Nov 15 2018 at 16:01):Now we have these .aux files, but they are a pain to handle
Emilio Jesús Gallego Arias (Nov 15 2018 at 16:02):time to introduce .vp files
Karl Palmskog (Nov 15 2018 at 16:02):what would they contain?
Karl Palmskog (Nov 15 2018 at 16:02):w.r.t. distributed systems, I have some hopes that there will be a big project based on distributed separation logics (shallow embedded by Sergey et al, deep by Birkedal et al), it solves a lot of code/proof composition issues we had with Verdi
Karl Palmskog (Nov 15 2018 at 16:03):btw @Emilio Jesús Gallego Arias are you coming to CoqPL by any chance?
Emilio Jesús Gallego Arias (Nov 15 2018 at 16:04):I will give the invited talk I think
Emilio Jesús Gallego Arias (Nov 15 2018 at 16:04):so yes :D :D
Karl Palmskog (Nov 15 2018 at 16:04):oh great
Emilio Jesús Gallego Arias (Nov 15 2018 at 16:04):I need to book my tickets tho
Karl Palmskog (Nov 15 2018 at 16:04):I will give a talk as well, hope we can chat a bit
Emilio Jesús Gallego Arias (Nov 15 2018 at 16:04):of course!
Emilio Jesús Gallego Arias (Nov 15 2018 at 16:04):fantastic!
Karl Palmskog (Nov 15 2018 at 16:04):we hope to join the consortium quite soon
Emilio Jesús Gallego Arias (Nov 15 2018 at 16:05):cool :) I am not up to date with that tho, this is Maxime's territory.
Karl Palmskog (Nov 15 2018 at 16:05):right, I think Zach Tatlock at UW will be in touch with Maxime
Emilio Jesús Gallego Arias (Nov 15 2018 at 16:05):Now you reminded me that I am very late with loads of admin stuff so I will be offline for a while
Emilio Jesús Gallego Arias (Nov 15 2018 at 16:05)::)
Karl Palmskog (Nov 15 2018 at 16:05):OK thanks again
Emilio Jesús Gallego Arias (Nov 15 2018 at 16:05):also going to this https://www.college-de-france.fr/site/xavier-leroy/inaugural-lecture-2018-2019.htm
Emilio Jesús Gallego Arias (Nov 15 2018 at 16:05):thanks to you!
Emilio Jesús Gallego Arias (Nov 15 2018 at 16:06):let me know how things are going with Dune, I shall write you "soon" by mail about incremental compilation by the way
Karl Palmskog (Nov 15 2018 at 16:06):great
Karl Palmskog (Nov 17 2018 at 04:10):so, apparently the Coq OPAM repo is not seeing a lot of attention lately, I think this is the longest turnaround time I've had for years
Karl Palmskog (Nov 17 2018 at 04:11):(for getting a PR merged)
Karl Palmskog (Nov 17 2018 at 04:12):still think having released packages for most contribs/community is a good idea
Théo Zimmermann (Nov 17 2018 at 09:33):@Karl Palmskog You might request @Enrico Tassi to put you in the opam-maintainers team so that you can merge PRs yourself...
Karl Palmskog (Nov 19 2018 at 02:54):I'm probably too much out of the loop w.r.t. CI practices, OPAM conventions, etc., to be a good maintainer there
Karl Palmskog (Nov 19 2018 at 16:26):@Théo Zimmermann so what should conventions be with branches/versions for community projects? Just a master branch that's backward compatible as far as reasonable, and then point to releases for anything else?
Karl Palmskog (Nov 19 2018 at 16:27):and releases whenever a new stable Coq version comes out that the last release is incompatible with?
Anton Trunov (Nov 19 2018 at 21:29):@Théo Zimmermann I just got an email notification from travis, saying that build passed — I just wanted to let you know that I like this feature and thanks a lot for taking care of this
Karl Palmskog (Nov 20 2018 at 21:59):so CI via Nix seems to be great when there's a tarball, like master and 8.8, but slow when there isn't, like for v8.9
Karl Palmskog (Nov 20 2018 at 22:00):or is there some magic way to get precompiled Coq 8.9 branch?
Karl Palmskog (Nov 20 2018 at 22:01):I tend to use pre-build Docker containers with a fixed Coq version, so haven't dealt with moving target...
Emilio Jesús Gallego Arias (Nov 20 2018 at 22:59):@Karl Palmskog you should ask @Théo Zimmermann , but I think that v8.9 has the right nix job to do the cachix thing https://gitlab.com/coq/coq/pipelines/34725732
Karl Palmskog (Nov 21 2018 at 00:21):OK, @Théo Zimmermann here is an example of a slow job, can we do anything to speed up by changing some Travis/Nix configuration line? https://travis-ci.com/coq-community/lemma-overloading/jobs/159911331
Théo Zimmermann (Nov 22 2018 at 10:55):@Karl Palmskog Sorry, I have been completely disconnected from Gitter during a workshop I was attending.
Théo Zimmermann (Nov 22 2018 at 10:56):Thanks for your questions. Indeed, you have a beginning of an answer in my reply to your review on GitHub.
Théo Zimmermann (Nov 22 2018 at 10:56):I'll try to sum up the rest of the situation later today and what I think are the ways to solve this.
Karl Palmskog (Nov 22 2018 at 17:33):sounds good
Karl Palmskog (Nov 22 2018 at 17:36):by the way, how casual are we with proposing new projects for moving into the community? I've come across several unmaintained plugins and the like that look interesting, but where I have no pressing need to use or motivation to maintain. It may still be worth documenting these for people who may want to learn-by-porting or similar.
Théo Zimmermann (Nov 22 2018 at 17:37):I think you should open an issue for them, and add the "maintainer-wanted" tag.
Théo Zimmermann (Nov 22 2018 at 17:37):We should not be afraid of adding many projects. It is OK if they end up unmaintained once again: in this case we mark them as such and "archive" them.
Théo Zimmermann (Nov 22 2018 at 18:00):Unfortunately the opening of the issue about Nix will have to wait tomorrow
Karl Palmskog (Nov 22 2018 at 18:46):OK, will open issues then
Karl Palmskog (Nov 22 2018 at 18:47):templates for README look good btw, just feel we could push OPAM packages more, there may be some other place for that though
Karl Palmskog (Nov 22 2018 at 20:48):are there best practices for -Q vs. -R in _CoqProject among Coq devs? We tend to use -Q, and I think uniformity in how one uses a module inside/outside a project (always qualify by namespace) is good.
Karl Palmskog (Nov 22 2018 at 20:51):for example, one could use the heuristic of: -Q unless -R is really needed due to need for branching directory structure
Anton Trunov (Nov 23 2018 at 09:05):@Karl Palmskog I think the manual would benefit from a bit clearer exlaination about these flags. Would be awesome if you had time to put some of your knowledge in there!
Théo Zimmermann (Nov 23 2018 at 14:22):@Karl Palmskog -Q is the recommended one indeed. I almost included template files for Makefile + _CoqProject with the -Q option but did not because the listing of the .v files is not something that one can do with just the template language.
Emilio Jesús Gallego Arias (Nov 23 2018 at 18:42):@Karl Palmskog see also dune/dune#1555
Emilio Jesús Gallego Arias (Nov 23 2018 at 18:42):when that is ready you will be able just to depend on libraries by name and you can forget about -Q/ -R
Karl Palmskog (Nov 23 2018 at 19:52):@Emilio Jesús Gallego Arias does that enable capturing extracted files as well?
Karl Palmskog (Nov 23 2018 at 19:53):sounds great even without that though
Anton Trunov (Nov 23 2018 at 19:56):@Emilio Jesús Gallego Arias coq support in dune! very cool!
Emilio Jesús Gallego Arias (Nov 23 2018 at 20:16):@Karl Palmskog yes we can add an (extracted_modules ...) field for sure
Emilio Jesús Gallego Arias (Nov 23 2018 at 20:17):in a sense that's not so different from native compilation, which produces ocaml files
Karl Palmskog (Nov 23 2018 at 21:05):for posterity, the right link is ocaml/dune#1555
Karl Palmskog (Nov 23 2018 at 21:14):I still think one should mostly use OPAM for managing Coq dependencies (e.g., git-based packages), although a composable build via Dune makes sense if one is co-developing several independent projects
Emilio Jesús Gallego Arias (Nov 23 2018 at 23:08):Note that Dune will generate OPAM packages / allow to specify external dependencies soon, so that is stricltly more general. But at the Coq build level, we cannot depend on OPAM.
Karl Palmskog (Nov 24 2018 at 12:20):hmm, I'm not sure that HTML processing of stuff inside template variables is what we want: https://raw.githubusercontent.com/coq-community/lemma-overloading/template-gen/README.md
Karl Palmskog (Nov 24 2018 at 12:21):I think it detracts from non-github readability to have a bunch of ", ' and the like
Théo Zimmermann (Nov 24 2018 at 12:21):There is a way to not preprocess : {{& }} (see the use with opam version constraints)
Karl Palmskog (Nov 24 2018 at 12:22):OK, then I think that that should be used for description and documentation at least
Théo Zimmermann (Nov 24 2018 at 12:22):Indeed.
Théo Zimmermann (Nov 24 2018 at 12:28):Feel free to push a commit fixing this without going through a PR.
Karl Palmskog (Nov 24 2018 at 12:30):OK will do
Karl Palmskog (Nov 27 2018 at 05:19):so here is a problem with the current README and opam template: there is no way to add new people as authors, because they will be listed as "Initial author(s)"
Karl Palmskog (Nov 27 2018 at 05:20):one may want to credit someone who is not an initial author, e.g., for doing refactoring, and then they should show up, e.g., in the OPAM file
Karl Palmskog (Nov 27 2018 at 05:21):I see two ways to solve this: (1) rename "Initial author(s)" to "Author(s)", or (2) introduce some other category, e.g., "Contributor(s)" that are also listed in the OPAM file
Karl Palmskog (Nov 30 2018 at 00:25):@Anton Trunov I think it was I that removed the old lemma-overloading branches (v8.5 and so on), but reading Théo's argument for preserving contrib history, maybe we should bring them back
Anton Trunov (Nov 30 2018 at 09:35):@Karl Palmskog We still have the corresponding tags, so restoring the branches might not be strictly necessary. E.g. we could put a tag on the last commit compatible with the corresponding Coq version. I guess with many more projects in coq-community we would not be able to do backporting due to the lack of manpower.
Anton Trunov (Nov 30 2018 at 09:36):But I’m fine with bringing the branches back if the coq-community members feel it’s useful.
Théo Zimmermann (Nov 30 2018 at 15:12):There's less tags than there were branches, no? Tips of branches before 8.5 did not have any corresponding tag. But that does not look like a big loss either.
Karl Palmskog (Dec 05 2018 at 21:36):so, are project website templates in a roadmap somewhere? I think the template MathComp uses (https://github.com/orderedlist/minimal) could be good with some small modifications
Karl Palmskog (Dec 05 2018 at 21:37):a real domain instead of coq-community.github.io would also be nice
Karl Palmskog (Dec 06 2018 at 21:22):@Anton Trunov could you check this Makefile template? https://github.com/coq-community/manifesto/wiki/Project-build-scripts
Karl Palmskog (Dec 06 2018 at 21:23):basically it's my adaptation of what most contribs are using, but your fcsl-pcm Makefile is a bit different, maybe you could explain the tradeoffs
Karl Palmskog (Dec 06 2018 at 21:24):in my testing I can't really see much of a difference in practice
Théo Zimmermann (Dec 10 2018 at 13:16):a real domain instead of
coq-community.github.iowould also be nice
Théo Zimmermann (Dec 10 2018 at 13:16):You think it would matter? If yes, we could ask the Coq Consortium to fund a domain name, this is quite cheap.
Anton Trunov (Dec 10 2018 at 13:54):@Karl Palmskog Sorry for the delay, we had a long holiday here. AFAIR, I copied that stub from https://coq.inria.fr/refman/practical-tools/utilities.html?highlight=coq_makefile#reusing-extending-the-generated-makefile
Théo Zimmermann (Dec 10 2018 at 13:54):Then I suppose the author of this is @Enrico Tassi.
Karl Palmskog (Dec 10 2018 at 18:14):OK I think I will do an issue on the Makefile thing and just ping him in
Karl Palmskog (Dec 10 2018 at 18:47):@Théo Zimmermann I mean, elf-community has a domain, right? It think it gives a sense of "this not just a few repos people casually maintain"
Karl Palmskog (Dec 10 2018 at 23:07):correction: http://elm-community.org
Théo Zimmermann (Dec 11 2018 at 09:20):Right. I will look into this.
Karl Palmskog (Dec 14 2018 at 21:41):so, should the documentation website + coqdoc live in a "web" directory or similar in the code branch like in mathcomp, or should it only live in the gh-pages branch?
Karl Palmskog (Dec 14 2018 at 21:43):maybe only basic static website files + generation scripts in master?
Théo Zimmermann (Dec 17 2018 at 15:52):GitHub pages support both the gh-pages branch setup and the docs/ sub-directory setup.
Théo Zimmermann (Dec 17 2018 at 15:53):The second one has the disadvantage to commit compilation outputs with the sources but seems much easier to manage.
Théo Zimmermann (Dec 17 2018 at 15:54):In particular, if the future of Coq packages is indeed to use Dune as a build system, then we will be able to rely on the "promote" rules that Dune has to automatically update the docs/ sub-directory when needed.
Karl Palmskog (Dec 17 2018 at 20:05):I think we should go with docs/ for now then
Théo Zimmermann (Dec 18 2018 at 08:23)::+1:
Karl Palmskog (Dec 26 2018 at 19:14):do we want Coq-community projects to use Proof using annotations? Even though they are kind of awkward to add/maintain, it seems that this is the only way to fully use fine-grained parallelism, even if the new vos/vok approach is adopted (coq/coq#8642)
Karl Palmskog (Dec 28 2018 at 01:47):would be nice if we had some general badge for linking to DOIs for papers. Like the Zenodo ones but without the Zenodo
Karl Palmskog (Jan 15 2019 at 09:10):@Théo Zimmermann just a ping about the domain thing (IMO, either coq-community.org or coq.community or both). If funding is an issue I wouldn't mind contributing.
Théo Zimmermann (Jan 16 2019 at 12:05):Funding should be OK as it is not much and Inria has some money. The more complex question is for instance who should be listed as an owner for this domain name, who should have access to the admin panel (even if obviously we only want it to point to GitHub pages)... It could either be an individual (me for instance), or we could have Inria purchase the domain in its own name. I asked about this at the last WG, and the answer was not clear to anyone. Maybe @Maxime Dénès can get info about this. He's not in this Gitter room but I'll ping him by PM.
Maxime Dénès (Jan 21 2019 at 11:04):I can try to investigate, indeed
Karl Palmskog (Feb 02 2019 at 15:47):@Théo Zimmermann I spoke briefly to Enrico at CoqPL about the SPDX thing. I think our consensus was that we should go ahead and start to use SPDX identifiers in the Coq OPAM repo right now, migrate old packages as we go along, and add CI checks for new packages
Théo Zimmermann (Feb 02 2019 at 15:48):Cool!
Karl Palmskog (Feb 02 2019 at 15:48):so I think I will do a manifesto PR to enable using identifier
Karl Palmskog (Feb 02 2019 at 15:48):and we should use it when rolling out releases of all Coq-community packages
Théo Zimmermann (Feb 02 2019 at 15:48):Yep, and probably remove the shortname at the same time, right?
Karl Palmskog (Feb 02 2019 at 15:49):yeah probably a good idea
Karl Palmskog (Feb 02 2019 at 15:49):I also think I will do a separate PR that generalizes some templates for use in Coq-contrib
Karl Palmskog (Feb 02 2019 at 15:49):(with Coq-community URLs still being default)
Karl Palmskog (Feb 02 2019 at 15:50):I think we should set some tentative goal to get most projects released for 8.9 in Feb
Théo Zimmermann (Feb 02 2019 at 15:52):I also think I will do a separate PR that generalizes some templates for use in Coq-contrib
Indeed, that cannot hurt.
Karl Palmskog (Feb 02 2019 at 15:52):I actually find a bunch of projects in contrib super useful, but no spare cycles to take over maintenance
Théo Zimmermann (Feb 02 2019 at 15:53):Yep, do not hesitate to open issues on the manifesto tracker though.
Théo Zimmermann (Feb 02 2019 at 15:53):When we have enough projects waiting for a maintainer, we might do a call on Coq-Club...
Karl Palmskog (Feb 02 2019 at 15:55):I think Maxime did quite good PR during CoqPL, but the best target group may be students (who've gotten through something like Software Foundations)
Théo Zimmermann (Feb 02 2019 at 15:55):I think we should set some tentative goal to get most projects released for 8.9 in Feb
We can try to start setting up some kind of automatic deploy in CI as suggested by Emilio in https://github.com/coq/bot/issues/30. I'm not sure how hard/easy that would be and how much it would help maintainers.
Karl Palmskog (Feb 02 2019 at 15:56):yeah I think that would be great if we can figure out more automation there.
Théo Zimmermann (Feb 02 2019 at 15:56):I think Maxime did quite good PR during CoqPL, but the best target group may be students (who've gotten through something like Software Foundations)
Yeah, I was thinking about students. And also about adding a mention to Coq's contributing guide for additional contribution suggestions. What do you mean by "PR" in this context?
Karl Palmskog (Feb 02 2019 at 15:56):advertisement
Karl Palmskog (Feb 02 2019 at 15:57):he had a slide calling for contributors basically
Théo Zimmermann (Feb 02 2019 at 15:57):Advertisement for coq-community specifically or for Coq in general?
Karl Palmskog (Feb 02 2019 at 15:57):for Coq-community
Théo Zimmermann (Feb 02 2019 at 15:58):Hey that's nice! Especially given that he was not so convinced initially :)
Théo Zimmermann (Feb 02 2019 at 15:58):BTW I am sorry I couldn't come to CoqPL, I will try harder to come to the Coq workshop.
Théo Zimmermann (Feb 02 2019 at 15:59):I still have a coupon to use to produce coq-community stickers, BTW. That comes from the winning of the logo.
Karl Palmskog (Feb 02 2019 at 15:59):cool, I will try to come as well
Théo Zimmermann (Feb 02 2019 at 16:00):(that's a $75 StickerMule voucher: https://www.stickermule.com/uses/open-source-stickers?utm_source=openlogos2018&utm_campaign=openlogos2018-sponsorship&utm_medium=referral)
Karl Palmskog (Feb 02 2019 at 16:01):until then I'll try to attend the workgroup meetings, although my French is super rusty
Théo Zimmermann (Feb 02 2019 at 16:01):However, I don't know if it expires.
Théo Zimmermann (Feb 02 2019 at 16:01):We don't usually speak French during WGs.
Théo Zimmermann (Feb 02 2019 at 16:02):At least, we make sure not to speak French if there is one non-French speaking person attending.
Théo Zimmermann (Feb 02 2019 at 16:02):But even when we are all French speakers, we sometimes prefer to speak in English to facilitate YouTube broadcasting.
Karl Palmskog (Feb 02 2019 at 16:03):OK that's nice, I try to watch at least some parts
Karl Palmskog (Feb 02 2019 at 16:07):oh, I think I can say this finally now, we've been working on mutation analysis of Coq projects via SerAPI and needed a bunch of good projects for experiments and Coq-community was a great source, so thanks @Théo Zimmermann
Théo Zimmermann (Feb 02 2019 at 16:07):Thanks for your active support!
Théo Zimmermann (Feb 02 2019 at 16:08):I've been looking a bit at your work with Emilio and your UT lab ;-)
Karl Palmskog (Feb 02 2019 at 16:08):without the CI would have been much harder (we were basically working against v8.9)
Théo Zimmermann (Feb 02 2019 at 16:09):I'm sad I didn't know about your team when I was at UT Austin for a year (but in the CS dept)...
Karl Palmskog (Feb 02 2019 at 16:09):I believe I was at UIUC when you were here
Karl Palmskog (Feb 02 2019 at 16:09):and my boss too
Théo Zimmermann (Feb 02 2019 at 16:09):Ah OK I didn't know your boss had moved recently!
Karl Palmskog (Feb 02 2019 at 16:10):I think he started in 2016
Karl Palmskog (Feb 02 2019 at 16:10):but there seems to be a lot of shuttle traffic between UIUC-UT, e.g., Tandy Warnow is now UIUC
Théo Zimmermann (Feb 02 2019 at 16:10):Yep, I know and she was my boss at UT Austin
Théo Zimmermann (Feb 02 2019 at 16:11):(during the second semester, after a strange first semester with the ACL2 team)
Karl Palmskog (Feb 02 2019 at 16:12):the only Coq-related people I know of now at UT are William Cook and Don Batory who did a bunch of work with Ben Delaware on product lines of theorems and other SE concepts in Coq
Théo Zimmermann (Feb 02 2019 at 16:12):I had classes with these two :)
Théo Zimmermann (Feb 02 2019 at 16:13):But Don was a strange guy, I didn't know he had worked with Coq
Théo Zimmermann (Feb 02 2019 at 16:13):I'm less surprised to hear that William Cook has. I learned Haskell in his class.
Karl Palmskog (Feb 02 2019 at 16:13):I think he didn't work with it directly, but he has/had students that use it for sure
Karl Palmskog (Feb 02 2019 at 16:14):I guess we do similar things in that we use SE methods for Coq. Main drawback is that SE conferences that are natural home for the research are not super positive about proof assistants.
Théo Zimmermann (Feb 02 2019 at 16:15):Yeah, it seems to me that there is a grand divide between SE and PL and people who are at the frontier do not feel like they belong.
Théo Zimmermann (Feb 02 2019 at 16:15):SPLASH looks like something that is a bit at the frontier though.
Karl Palmskog (Feb 02 2019 at 16:15):at POPL people were really positive about better tooling, but obviously tool papers are not their niche
Théo Zimmermann (Feb 02 2019 at 16:16):TBH I am only starting to discover the SE domain as it's not really my supervisor area but this is what I want to focus on.
Karl Palmskog (Feb 02 2019 at 16:16):yeah OOPSLA may be the best middle ground.
Karl Palmskog (Feb 02 2019 at 16:19):@Théo Zimmermann any specific form of SE? we obviously look a lot at the "evolutionary" form (CI, incrementality, revisions, ...)
Théo Zimmermann (Feb 02 2019 at 16:21):The whole field is pretty new to me but I'm looking quite a lot into studies on the open source development model.
Théo Zimmermann (Feb 02 2019 at 16:21):I've just submitted a paper to MSR (Mining Software Repositories).
Théo Zimmermann (Feb 02 2019 at 16:21):This is associated to ICSE.
Karl Palmskog (Feb 02 2019 at 16:22):ah, we've talked about "mining proof repositories" stuff here
Théo Zimmermann (Feb 02 2019 at 16:22):Ah that's cool. Do you have a pointer?
Karl Palmskog (Feb 02 2019 at 16:22):there are some papers in that direction, like metrics for proofs
Théo Zimmermann (Feb 02 2019 at 16:23):I would be interested in pointers in research on CI too.
Karl Palmskog (Feb 02 2019 at 16:23):hmm, I'm aware of at least a few, but there's a lot of different niches there
Karl Palmskog (Feb 02 2019 at 16:24):I can send an email with some stuff
Théo Zimmermann (Feb 02 2019 at 16:24):Thanks!
Karl Palmskog (Feb 02 2019 at 16:24):I assume the paris-diderot email?
Théo Zimmermann (Feb 02 2019 at 16:24):Yep, that one is good.
Karl Palmskog (Feb 02 2019 at 16:39):it's interesting to compare Coq and Isabelle w.r.t. maintenance and so on. The Isabelle Archive of Formal Proofs is great, but it's very much an "in or out" situation
Karl Palmskog (Feb 02 2019 at 16:39):either your project is in it and gets immediate updates for every conceivable change, or you're outside and will rot away
Théo Zimmermann (Feb 02 2019 at 16:40):Yes. And getting "in" supposes having already attained a certain level of maturity.
Karl Palmskog (Feb 02 2019 at 16:40):I think Coq is lacking a bit of certification though, their reviewing gives a lot of respectability
Théo Zimmermann (Feb 02 2019 at 16:41):Yes, that's why the coq-community project has this idea of an "editorial committee".
Karl Palmskog (Feb 02 2019 at 16:41):I mean, we know that there are projects that are just so much above the standard project, but it's not like it's obvious which ones they are to outsiders
Théo Zimmermann (Feb 02 2019 at 16:41):But I have not been making any progress on that front by lack of time mainly.
Karl Palmskog (Feb 02 2019 at 16:41):oh, right, you were thinking of that with Pierre [Casteran] right?
Théo Zimmermann (Feb 02 2019 at 16:42):Yes, and some others like Bas Spitters.
Karl Palmskog (Feb 02 2019 at 16:42):Jasmin Blanchette says he wants to do an AFP for Lean as well
Karl Palmskog (Feb 02 2019 at 16:43):I think the Isabelle AFP is just so absurdly tight with Isabelle development, both Coq and Lean could be a bit more loose
Théo Zimmermann (Feb 02 2019 at 16:44):AFP might not be the right model for a new proof assistant. But there is still work for me to prove that I have something better to propose :wink:
Théo Zimmermann (Feb 02 2019 at 16:45):That being said, Lean might not be yet in a state were they can manage backward compatibility.
Théo Zimmermann (Feb 02 2019 at 16:45):And then, this tight link with the development might make sense.
Karl Palmskog (Feb 02 2019 at 16:45):AFP also fills the function of providing "academic cover" for just doing the actual proof work
Théo Zimmermann (Feb 02 2019 at 16:45):(like for Coq and its plugins)
Karl Palmskog (Feb 02 2019 at 16:45):one can put in one's CV that project so-and-so got into the archive
Théo Zimmermann (Feb 02 2019 at 16:46):OK, it was not clear to me if that was enough for people, or if they always used it as a companion to a real publication
Karl Palmskog (Feb 02 2019 at 16:47):I think it's both, I know Jasmin tends to emphasize both
Karl Palmskog (Feb 02 2019 at 16:47):like IsaFOL, it's so many papers at this point
Karl Palmskog (Feb 02 2019 at 16:48):so the best single reference is what's in AFP
Théo Zimmermann (Feb 02 2019 at 16:51):Thanks for your mail!
Karl Palmskog (Feb 02 2019 at 16:53)::thumbsup:
Karl Palmskog (Feb 05 2019 at 15:34):@Théo Zimmermann Adam Chlipala said he attempted the transfer of Chapar, did you see anything as GitHub org owner?
Karl Palmskog (Feb 05 2019 at 22:12):@Théo Zimmermann I told Adam to try to transfer the Chapar repo to your personal account (always works), then you can transfer to Coq-community
Karl Palmskog (Feb 05 2019 at 22:13):I think we need some checklist there
Karl Palmskog (Feb 05 2019 at 22:55):oh, that failed too, see email
Théo Zimmermann (Feb 06 2019 at 07:41):I didn't see anything. You can normally always transfer directly, a repository you are admin of, to an organization on which you have permission to create a repo.
Karl Palmskog (Feb 06 2019 at 19:23):@Théo Zimmermann Adam Chlipala says he still doesn't have privileges on coq-community, could you double check an invite has been sent?
Théo Zimmermann (Feb 07 2019 at 10:31):@Karl Palmskog There is a pending invitation for @achlipala. He can accept it by going to https://github.com/coq-community.
Théo Zimmermann (Feb 07 2019 at 10:31):Adam has two accounts. I did not invite his -biz account.
Karl Palmskog (Feb 07 2019 at 14:29)::thumbsup:
Karl Palmskog (Feb 07 2019 at 21:12):btw there are so many future tasks related to SPDX I'm going to keep the issue open
Théo Zimmermann (Feb 07 2019 at 21:13):ok
Karl Palmskog (Feb 07 2019 at 21:17):since the cat is out of the bag on mutation using SerAPI in Coq now, I'm probably going to add some results as issues to Coq-community projects
Théo Zimmermann (Feb 07 2019 at 21:17):cool :+1:
Karl Palmskog (Feb 07 2019 at 21:17):basically, most unkilled mutants are not bugs but kind of about dangling definitions
Karl Palmskog (Feb 07 2019 at 21:18):arguably, one might want to not have a bunch of random data and functions unconnected to the main purpose of the library
Karl Palmskog (Feb 07 2019 at 21:18):but it depends on the context
Théo Zimmermann (Feb 07 2019 at 21:19):What about unused lemmas? Are they flagged too?
Karl Palmskog (Feb 07 2019 at 21:19):we didn't mutate lemma statements this time
Karl Palmskog (Feb 07 2019 at 21:20):might be better to use something like dpdgraph there
Théo Zimmermann (Feb 07 2019 at 21:20):I see
Karl Palmskog (Feb 07 2019 at 21:21):but it may make sense for some projects
Karl Palmskog (Feb 07 2019 at 21:21):I just couldn't find a good way to justify it in the paper
Karl Palmskog (Feb 07 2019 at 21:22):the functions+data vs. spec dichotomy is strong in the SE world, but not so much in math+theoretical CS
Karl Palmskog (Feb 07 2019 at 21:23):I think the number of mutants could have become ridiculously large also, but I think we'll do some more experiments this spring.
Emilio Jesús Gallego Arias (Feb 08 2019 at 01:19):since the cat is out of the bag on mutation using SerAPI in Coq now, I'm probably going to add some results as issues to Coq-community projects
Not really tho, only people at CoqPL know about it
Emilio Jesús Gallego Arias (Feb 08 2019 at 01:20):that is Maxime and Enrico, I think Enrico got confused with the iCoq paper today
Karl Palmskog (Feb 08 2019 at 15:38):@Théo Zimmermann I'm going to merge some meta + opam + doc stuff for Hugo's Coq-community projects, I don't think he'll mind, right?
Théo Zimmermann (Feb 08 2019 at 15:47):He won't mind.
Karl Palmskog (Feb 10 2019 at 02:18):I think it's time to write a template for OPAM2 files
Karl Palmskog (Feb 10 2019 at 02:18):some packages should probably go into extra-dev
Théo Zimmermann (Feb 10 2019 at 17:00):Is there any way of having opam1 and opam2 files co-exist in a repo? Otherwise, I guess we'll just have to have a switch to decide which version to use...
Théo Zimmermann (Feb 10 2019 at 17:01):I don't remember if you were there when Enrico told this in the WG but the plan is to migrate the released opam repo to opam2 during the 8.10 beta.
Karl Palmskog (Feb 10 2019 at 17:14):yeah I heard that. We could always have some convention like <name>.opam2.
Karl Palmskog (Feb 10 2019 at 17:15):the annoying thing about opam2 is they have both a synopsis and description field
Karl Palmskog (Feb 10 2019 at 17:16):I'm not sure either of them can/should contain Markdown
Karl Palmskog (Feb 10 2019 at 17:45):one possible take: we do a synopsis field in meta.yml which is a one-liner that should be used in the GitHub repo description and should mention Coq
Karl Palmskog (Feb 10 2019 at 17:46):then we just use the description field from meta.yml as is
Karl Palmskog (Feb 10 2019 at 17:47):maybe one could automate synchronizing repo descriptions with synopsis at some point
Théo Zimmermann (Feb 10 2019 at 19:56)::+1: sounds doable
Karl Palmskog (Feb 16 2019 at 23:17):OPAM2 migration heating up: https://github.com/coq/opam-coq-archive/pull/587
Karl Palmskog (Feb 19 2019 at 18:53):so it seems like an odious requirement to not have OCaml warnings in old plugins
Emilio Jesús Gallego Arias (Feb 19 2019 at 18:54):What do you mean @Karl Palmskog ?
Karl Palmskog (Feb 19 2019 at 18:54):I would be in favor of not having such Coq-community plugins in Coq's CI
Emilio Jesús Gallego Arias (Feb 19 2019 at 18:54):why is it odious?
Karl Palmskog (Feb 19 2019 at 18:54):I mean, assume maintainership and suddenly you have to refactor a lot of internals
Karl Palmskog (Feb 19 2019 at 18:54):even though the plugin works
Emilio Jesús Gallego Arias (Feb 19 2019 at 18:55):I don't think large changes are needed, most warning are either serious bugs, or trivial to fix
Emilio Jesús Gallego Arias (Feb 19 2019 at 18:55):but indeed see the discussion in the issue, allowing some warnings to go thru introduced serious bugs in almost all plugins
Emilio Jesús Gallego Arias (Feb 19 2019 at 18:55):for example with the merge of primitive integers
Emilio Jesús Gallego Arias (Feb 19 2019 at 18:56):also disabling warnings in your plugin is usually OK
Emilio Jesús Gallego Arias (Feb 19 2019 at 18:56):keep in mind that Coq people does maintain plugins these days, as we submit the overlays
Emilio Jesús Gallego Arias (Feb 19 2019 at 18:56):even though the plugin works
I wish this was the case but my lastest overlay rounds I did find many serious bugs signaled by warnings
Karl Palmskog (Feb 19 2019 at 18:56):the aac-tactics warnings have been around for ages and are all over the codebase
Emilio Jesús Gallego Arias (Feb 19 2019 at 18:57):let me look into that one
Emilio Jesús Gallego Arias (Feb 19 2019 at 18:57):we can of course disable that warning for acc-tactics
Théo Zimmermann (Feb 19 2019 at 18:57):it would be great to actually find which warnings are the most pressing to fix
Karl Palmskog (Feb 19 2019 at 18:57):I can't look at it in the near future in any case, so any changes welcome
Théo Zimmermann (Feb 19 2019 at 18:58):a problem with the way you formulated your issue @Emilio Jesús Gallego Arias is that you don't really give a timeline (obviously you can't because nothing is decided)
Théo Zimmermann (Feb 19 2019 at 18:59):but it would have been good to formulate in a different way "could you try to see if you can fix ? / we can help if needed"...
Karl Palmskog (Feb 19 2019 at 18:59):yeah I think it would be great to say, after 8.10 release we will require this
Théo Zimmermann (Feb 19 2019 at 18:59):not a real critic, I have done the same thing in the past
Théo Zimmermann (Feb 19 2019 at 18:59):with warnings too
Karl Palmskog (Feb 19 2019 at 18:59):so I can plan to spend time
Emilio Jesús Gallego Arias (Feb 19 2019 at 19:01):yeah see my comments here https://github.com/QuickChick/QuickChick/issues/143
Emilio Jesús Gallego Arias (Feb 19 2019 at 19:02):acc-tactics dies on an comment warning
Emilio Jesús Gallego Arias (Feb 19 2019 at 19:02):these ones are trivial to fix
Karl Palmskog (Feb 19 2019 at 19:07):sure, but there are lots of incomplete matching warnings
Emilio Jesús Gallego Arias (Feb 19 2019 at 19:08):let me check a non failing build
Théo Zimmermann (Feb 19 2019 at 19:08):Note that @Fabian Kunze has announced his intention to redesign part of the plugin, so some warnings could also disappear that way (but I don't know about the timeline)
Emilio Jesús Gallego Arias (Feb 19 2019 at 19:09):sure, but there are lots of incomplete matching warnings
I don't see any @Karl Palmskog https://gitlab.com/coq/coq/-/jobs/164033445
Emilio Jesús Gallego Arias (Feb 19 2019 at 19:09):where do you see them?
Karl Palmskog (Feb 19 2019 at 19:27):OK maybe I mixed it up with some other plugin, or some Coq level warning
Emilio Jesús Gallego Arias (Feb 19 2019 at 19:31):Ok, let me know if you think this is a problem on some other plugin
Karl Palmskog (Feb 23 2019 at 04:14):I think we should do what we can for the poor coq-contrib projects, I have used many of them in the past, taking the first steps now
Karl Palmskog (Mar 02 2019 at 21:04):@Théo Zimmermann could be a good idea to have a general "Call for Coq-community contributors" in the Discourse announcements?
Karl Palmskog (Mar 03 2019 at 20:05):so here's an idea I've thought about for some time: mining Coq project tarballs from the web
Karl Palmskog (Mar 03 2019 at 20:06):there's just so much Coq code out there that's not on GitHub but are on some researcher's personal website
Karl Palmskog (Mar 03 2019 at 20:08):probably one could write a spider to look for links in Coq-related papers, download tarballs, and look for .v files
Emilio Jesús Gallego Arias (Mar 03 2019 at 20:50):I have a personal archive @Karl Palmskog , each project I've come across then I download it, 188 so far
Karl Palmskog (Mar 03 2019 at 22:03):nice
Théo Zimmermann (Mar 04 2019 at 16:15):@Karl Palmskog I would like to do this, but first we should expand our list of projects looking for a maintainer, and second we should wait that for Discourse to be a bit more populated.
Théo Zimmermann (Mar 04 2019 at 16:16):We only have 122 users so far.
Karl Palmskog (Mar 04 2019 at 17:01)::thumbsup:
Karl Palmskog (Mar 04 2019 at 17:36):I got Chapar to work with 8.9+master at least... although the OCaml part still needs revision
Karl Palmskog (Mar 04 2019 at 17:37):it's going to need some thought how to set up Travis for OCaml subprojects, e.g., one does not want to have OCaml package dependencies for the Coq part
Karl Palmskog (Mar 05 2019 at 01:36):with only 3 weeks until OPAM 2 upgrade, I guess we should phase out OPAM1.2 files/template
Karl Palmskog (Mar 07 2019 at 20:56):@Théo Zimmermann I want to test the templates with a Coq-contrib project, which one would you recommend? Do they all have Travis enabled?
Théo Zimmermann (Mar 08 2019 at 10:03):None of them have Travis enable. Let me change this.
Théo Zimmermann (Mar 08 2019 at 10:08):Alright, @Karl Palmskog that's done. I'll also add you as a member to the coq-contribs organization to give you push access everywhere.
Karl Palmskog (Mar 08 2019 at 12:58)::thumbsup:
Karl Palmskog (Mar 11 2019 at 16:04):one thing that's missing now is to write a converter from description to meta.yml
Karl Palmskog (Mar 11 2019 at 16:05):with that, contribs can be made to look like this and become much easier to adopt into Coq-community: https://github.com/coq-contribs/quicksort-complexity
Théo Zimmermann (Mar 12 2019 at 21:14):Yes, that would be useful but I don't think this is actually something that can be fully mechanized.
Théo Zimmermann (Mar 12 2019 at 21:15):FTR, public domain != the Unlicense but you know this already from https://github.com/coq-community/manifesto/issues/38#issuecomment-469614018
Karl Palmskog (Mar 12 2019 at 21:21):sure, I took the best approximation, the license in description was already inconsistent with LICENSE
Karl Palmskog (Mar 12 2019 at 21:22):@Théo Zimmermann so what string should we use for public domain then, as a policy?
Karl Palmskog (Mar 12 2019 at 21:23):I would generally vote for "relicensing" under Unlicense
Karl Palmskog (Mar 12 2019 at 21:25):maybe you've already seen https://wiki.spdx.org/view/Legal_Team/Decisions/Dealing_with_Public_Domain_within_SPDX_Files
Karl Palmskog (Mar 12 2019 at 21:54):in my reading, any "summary" of a public domain dedication can be considered not well defined, for example, just saying "Public Domain" doesn't solve the problem
Théo Zimmermann (Mar 13 2019 at 12:10):We should add this data to #38. I'd vote for relicensing too. I would though only apply this decision for packages that are under the coq-community umbrella, in coordination with the maintainer. coq-contribs doesn't just have the problem of packages with unclear public domain dedications, it also has the (frequent) problem of packages with no license. If you want to use the README template for these projects, you'll have to find a solution that works in all these cases.
Karl Palmskog (Mar 13 2019 at 16:51):it's not like I enforce identifier to have some format yet, and personally I'm content with having a solution only for the more high-profile coq-contrib projects
Théo Zimmermann (Mar 14 2019 at 09:37)::+1:
Karl Palmskog (Mar 15 2019 at 00:22):we should probably think about doing "semi-manual" releases for 8.9 of the community projects at this point
Karl Palmskog (Mar 15 2019 at 00:22):I would say as soon as the OPAM repo migrates to OPAM2
Théo Zimmermann (Mar 15 2019 at 11:05):There are two cases to consider though:
Théo Zimmermann (Mar 15 2019 at 11:06):I am wary of too much automation though. The point of coq-community was not to reproduce coq-contribs.
Karl Palmskog (Mar 15 2019 at 14:49):I think many (most?) 8.8 packages are incompatible due to the Implicit Arguments deprecation
Karl Palmskog (Mar 15 2019 at 15:36):I would argue for "libertarian paternalism": provide automation tools to maintainers to follow best practices, but don't require people to use them
Karl Palmskog (Mar 15 2019 at 15:37):... only give nudges, such as saying that it will save time, etc.
Karl Palmskog (Mar 16 2019 at 00:14):we should probably start to use coq-<shortname>.opam rather than just opam, if there are several OPAM files present the CI will try to build them all in parallel...
Karl Palmskog (Mar 16 2019 at 00:14):with coq-<shortname>.opam one can do opam pin add coq-<shortname> . in CI
Théo Zimmermann (Mar 17 2019 at 20:44):Indeed, that would be better, but not something that we can really account for in the template proper. Except by changing the documented script for generating all the templates.
Karl Palmskog (Mar 17 2019 at 22:12):hmm, I think the Cachix-Coq is stale: https://github.com/coq/coq-on-cachix
Karl Palmskog (Mar 17 2019 at 22:12):not updated for 7 days
Karl Palmskog (Mar 17 2019 at 22:12):this makes CI fail for my nice plugin port to handle SProp changes...
Théo Zimmermann (Mar 18 2019 at 08:57):fixed
Karl Palmskog (Mar 18 2019 at 14:57)::thumbsup:
Karl Palmskog (Mar 21 2019 at 18:18):@Théo Zimmermann you've probably already seen these, but just to double-check: https://sketis.net/2017/social-networks-in-the-isabelle-and-coq-community https://arxiv.org/abs/1609.07127
Théo Zimmermann (Mar 21 2019 at 22:18):I hadn't seen the blog post but I did read the paper when it appeared.
Théo Zimmermann (Mar 21 2019 at 22:19):But thanks for sharing. I could share a few more thoughts but that would have to be in private.
Karl Palmskog (Mar 22 2019 at 17:15):@Théo Zimmermann can you invite this guy to the Coq-community GitHub organization, he showed some interest in having one of his projects co-maintained in the organization: https://github.com/vrahli/
Théo Zimmermann (Mar 24 2019 at 17:38)::+1:
Karl Palmskog (Apr 03 2019 at 16:53):@Théo Zimmermann with OPAM2 rolled out for released packages, I think it's reasonable to do 8.9 releases for Coq-community projects (at least the low-hanging fruit maintained by me/Hugo/etc.)
Karl Palmskog (Apr 03 2019 at 16:53):or what do you think?
Emilio Jesús Gallego Arias (Apr 03 2019 at 16:55):By the way Dune 1.9 (due in a few days) will support dune-release workflow for those interested
Emilio Jesús Gallego Arias (Apr 03 2019 at 16:55):I am not sure how to make dune-release submit to the coq opam repos instead of the main one tho
Karl Palmskog (Apr 03 2019 at 16:55):@Emilio Jesús Gallego Arias so what is included in that workflow? actually creating release on GitHub?
Emilio Jesús Gallego Arias (Apr 03 2019 at 16:55):opam pin add dune --dev allows you to test that now
Emilio Jesús Gallego Arias (Apr 03 2019 at 16:56):the workflow does everything: builds, run the tests, builds the package, updates the opam file, creates the github release and repository PR
Karl Palmskog (Apr 03 2019 at 16:56):and the PR target is configurable?
Emilio Jesús Gallego Arias (Apr 03 2019 at 16:56):that's my question, in the past it was
Emilio Jesús Gallego Arias (Apr 03 2019 at 16:57):but they tweaked some things, dune-release / to-pkg has the notion of backends
Emilio Jesús Gallego Arias (Apr 03 2019 at 16:57):so it shouldn't be too hard
Karl Palmskog (Apr 03 2019 at 16:57):so maybe the main drawback is that the project has to be dunerized?
Emilio Jesús Gallego Arias (Apr 03 2019 at 16:58):yes it is designed for that
Emilio Jesús Gallego Arias (Apr 03 2019 at 16:58):you can use opam-publish / topkg otherwise
Emilio Jesús Gallego Arias (Apr 03 2019 at 16:58):I dunno if anyone has written support for coq_makefile
Karl Palmskog (Apr 03 2019 at 16:58):OK, then I would probably vote for aiming to use that for 8.10 releases
Karl Palmskog (Apr 03 2019 at 16:58):and use opam-publish for now
Emilio Jesús Gallego Arias (Apr 03 2019 at 16:59):it is experimental of course, but if anyone is interested
Emilio Jesús Gallego Arias (Apr 03 2019 at 16:59):I use dune-release / Dune for all my ocaml projects and I am happy
Karl Palmskog (Apr 03 2019 at 16:59):am interested but it should probably be tried on some small project
Karl Palmskog (Apr 03 2019 at 16:59):is the Coq support in 1.9 as well?
Emilio Jesús Gallego Arias (Apr 03 2019 at 16:59):basically I had never to care about things
Emilio Jesús Gallego Arias (Apr 03 2019 at 16:59):yup
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:00):sorry, the Coq support is what is in 1.9
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:00):dune-release has been there since a lot
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:00):so with Dune 1.9
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:00):if you add the Dune files to a Coq project, you can just run dune-release and have everything done
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:01):provided there are no bugs or course :crossed_flags:
Karl Palmskog (Apr 03 2019 at 17:01):@Emilio Jesús Gallego Arias I think I'd try it first on some small coq-contrib and go from there
Karl Palmskog (Apr 03 2019 at 17:03):I think it's obvious most Coq-community projects will want to migrate to Dune but at their own pace
Karl Palmskog (Apr 03 2019 at 17:03):also nice to show people a commit: here is what you need to do to port your project with legacy build system
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:04):there is quite a few documentation both in the Coq , Dune manual, on discourse too
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:04):https://dune.readthedocs.io/en/latest/coq.html
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:04):of course improvements welcome
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:04):https://coq.discourse.group/t/a-guide-to-building-your-coq-libraries-and-plugins-with-dune/20
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:04):pity in discouse it seems we cannot assign a post to two categories
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:05):also Dune release notes will contaian a small example
Karl Palmskog (Apr 03 2019 at 17:05):sure, but not sure what the bottom line was there, e.g., one needs to keep -R flags in _CoqProject
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:05): Emilio Jesús Gallego Arias (Apr 03 2019 at 17:05):?
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:06):_CoqProject is not taken into account
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:06):you never use -Q or -R flags with Dune, that's the whole point
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:06):it takes care of it
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:06):maybe should be in the F.A.Q.
Karl Palmskog (Apr 03 2019 at 17:06):but what about CoqIDE/ProofGeneral?
Karl Palmskog (Apr 03 2019 at 17:06):I just want to clone a project, build it, then start to modify files
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:07):Oh good point, I guess I should submit a PR to GP
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:07):to PG
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:07):as for CoqIDE
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:07):I dunno
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:07):indeed that's a todo
Karl Palmskog (Apr 03 2019 at 17:07):so then one should arguably: delete the file list from _CoqProject, but keep the flags
Karl Palmskog (Apr 03 2019 at 17:07):for compatibility
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:07):not only that, but the build hygiene will mean these tools don't find the path
Karl Palmskog (Apr 03 2019 at 17:08):oh, so .vo files end up somewhere else
Karl Palmskog (Apr 03 2019 at 17:09):then you really need that PG patch
Karl Palmskog (Apr 03 2019 at 17:10):I think it's a very common workflow to clone + build + open file in emacs/PG
Karl Palmskog (Apr 03 2019 at 17:11):I think some projects then might even want to enable building with both coq_makefile and dune until the community has switched fully
Karl Palmskog (Apr 03 2019 at 17:13):I would argue keeping the Makefile is good in any case, since many people likely don't even know dune install
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:16):I think some projects then might even want to enable building with both coq_makefile and dune until the community has switched fully
Not a lot of reason to do that as the installs are compatible
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:16):oh, so .vo files end up somewhere else then you really need that PG patch
Yup I need a patch that calls dune coqtop dir to edit a file on that dir
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:17):Yes keeping a Makefile as a wrapper is customary
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:19):Actually we could even do dune coqtop --file=foo.v and would make sure that all deps are up to date
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:19):needs more discussion as merlin / OCaml people are implementhing heavier protocols for this
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:19):But you are right for now I've only worried about batch-building
Karl Palmskog (Apr 03 2019 at 17:20):so flags like -arg -w -arg -notation-overridden are handled by dune as well, right?
Karl Palmskog (Apr 03 2019 at 17:20):I think we need a way to communicate those to PG/CoqIDE
Karl Palmskog (Apr 03 2019 at 17:21):I wonder how dune will sit with the MIT people, who I think are using git submodules and flags like -R with paths
Karl Palmskog (Apr 03 2019 at 17:21):for dependency management
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:29):so flags like -arg -w -arg -notation-overridden are handled by dune as well, right?
Yes, you just invoke coqtop wrapped with IDE.
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:29):I wonder how dune will sit with the MIT people, who I think are using git submodules and flags like -R with paths
As far as I understand it will be a blessing for them.
Karl Palmskog (Apr 03 2019 at 17:30):my point about a project having both dune and coq_makefile installs is that some of your tooling could assume paths to .vo files
Karl Palmskog (Apr 03 2019 at 17:31):so you might want to use dune for batch-building and installs
Karl Palmskog (Apr 03 2019 at 17:32):I also want to look at the extraction story
Karl Palmskog (Apr 03 2019 at 17:33):for example, I have a bunch of custom rules that <extraction-dep>.vo must be built before we run coqc extraction.v which produces myfile.ml
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:33):my point about a project having both dune and coq_makefile installs is that some of your tooling could assume paths to .vo files
so you might want to use dune for batch-building and installs
I am not sure what you mean here, Dune is designed to install in a compatible way with coq_makefile projects, for the v1 version of the lang
Karl Palmskog (Apr 03 2019 at 17:34):with .vo files hygienized the extraction build rules won't work
Karl Palmskog (Apr 03 2019 at 17:35):installing is not the only goal of building
Karl Palmskog (Apr 03 2019 at 17:35):I might just want to obtain a single .vo file and have it live alongside .v, because some ad-hoc script assumes it
Karl Palmskog (Apr 03 2019 at 17:36):so I dunerize my project but keep the possibility of building with coq_makefile in my Makefile
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:45):or you can promote a file; but in general it is just easier to run the ad-hoc script in the install context
Emilio Jesús Gallego Arias (Apr 03 2019 at 17:46):if you call it from the Dune file it will think the .vos are there; at least for version 1.0
Karl Palmskog (Apr 03 2019 at 19:20):per the manual, there is no way to use -Q in coq-dune?
Emilio Jesús Gallego Arias (Apr 03 2019 at 20:08):What does "using -Q" mean?
Emilio Jesús Gallego Arias (Apr 03 2019 at 20:08):But indeed, wrapper modules are compiled with -R so you don't have to use the wrapper, à la OCaml
Emilio Jesús Gallego Arias (Apr 03 2019 at 20:09):however when depending on them they will be targetted with -Q
Emilio Jesús Gallego Arias (Apr 03 2019 at 20:09):so they are wrapped
Emilio Jesús Gallego Arias (Apr 03 2019 at 20:09):this needs refinement in the next PR
Emilio Jesús Gallego Arias (Apr 03 2019 at 20:10):I'll open an issue about that actually
Karl Palmskog (Apr 03 2019 at 21:06):OK I see
Emilio Jesús Gallego Arias (Apr 03 2019 at 23:31):Yup that's not very well explained I think; please open issues for bad documentation
Emilio Jesús Gallego Arias (Apr 03 2019 at 23:31):You can override the flags but that's not advised, as it won't work on the 2.0 version of the lang
Emilio Jesús Gallego Arias (Apr 03 2019 at 23:32):Dune + Coq 2.0 will install dune packages with the metadata and that should allow fancy stuff
Théo Zimmermann (Apr 04 2019 at 07:25):@Karl Palmskog The best way to integrate the Dune build with custom scripts is to add a custom build rule within the dune file that explicitly calls the script on the right dependencies. Dune will copy all the required files in the build directory, and if some dependencies need to be built first, it will build them, then it will call the script. If later on, you want to move back some build results (such as extraction outputs) to the tree, then you can use promote rules indeed.
Théo Zimmermann (Apr 04 2019 at 07:27):@Karl Palmskog Regarding your initial question, I don't remember what was the motivation for waiting for the switch to opam 2.0 to do the releases, but indeed, it's probably a good idea to do some releases for 8.9 now, even if that must be manual (it's only a few packages after all). And we can try afterwards to start moving packages to Dune and piggy-back on dune-release.
Emilio Jesús Gallego Arias (Apr 04 2019 at 12:02):Something I need to finish is coqdoc coq2ht ml support. Should be easy however I need to finish the composition patch first. I introduced a "virtual" .va file as to allow users to build a single lib, and that's what you want IMHO for doc.
Emilio Jesús Gallego Arias (Apr 04 2019 at 15:00):@Karl Palmskog can you open an issue about extraction support in Dune ? Thanks!
Karl Palmskog (Apr 04 2019 at 16:34):@Emilio Jesús Gallego Arias will do
Emilio Jesús Gallego Arias (Apr 04 2019 at 16:56):thanks @Karl Palmskog
Anton Trunov (Apr 12 2019 at 13:07):@Emilio Jesús Gallego Arias @Karl Palmskog Just noticed this discussion, folks :) As I mentioned in coq/coq today, I was experimenting with dunerizing a Coq library (fcsl-pcm).
So far I can make it work with one global dune at the project root file with (include_subdirs qualified) mechanizm.
There is already mentioned issue with PG, which could be worked around with opam install . command (basically using it instead of make). Unfortunately, it would only woks for small projects, as opam recompiles everything from scratch after every change.
Still, I like very much the direction the tooling is going! Kudos to Emilio!
Emilio Jesús Gallego Arias (Apr 12 2019 at 14:01):Thanks @Anton Trunov , I will add proper PG / CoqIDE support soon; for now I'm afraid that Dune is most useful for compilation.
Emilio Jesús Gallego Arias (Apr 12 2019 at 14:01):Adding interactive support is next on my todo list, but I need first to get composition sorted out [which mostly is]
Anton Trunov (Apr 12 2019 at 14:19):Makes sense, @Emilio Jesús Gallego Arias. Keeping my fingers crossed :)
Théo Zimmermann (Apr 15 2019 at 08:08):@Anton Trunov In a recent test of building a Coq project with Dune, I changed the _CoqProject line so that it would find where to look for compiled files: https://github.com/Zimmi48/huffman/commit/baade609aea67f8977f5954be9465ba3c38a50c3#diff-9962f476442d017ffc92f6c95391d7beR1
Théo Zimmermann (Apr 15 2019 at 08:09):Obviously, this is a hack until there is better editor support.
Emilio Jesús Gallego Arias (Apr 15 2019 at 08:37):@Théo Zimmermann you can also extend COQPATH with _build/install/lib/coq/user-contrib I think; indeed the question of how to properly integrate with editors is still a bit open also for OCaml
Anton Trunov (Apr 15 2019 at 09:58):@Théo Zimmermann @Emilio Jesús Gallego Arias Thank you both for your suggestion!
Emilio Jesús Gallego Arias (Apr 15 2019 at 10:00):Generating _CoqProject files is a bit ugly, as in particular it breaks build hygiene
Théo Zimmermann (Apr 15 2019 at 11:29):@Emilio Jesús Gallego Arias
Generating _CoqProject files is a bit ugly, as in particular it breaks build hygiene
Théo Zimmermann (Apr 15 2019 at 11:29):But this is how it works for .merlin. Not saying it's the perfect solution but it's good enough to start with.
Emilio Jesús Gallego Arias (Apr 15 2019 at 12:15):.merlin has many other problems, so we better try to jump into the next integration system.
Karl Palmskog (May 03 2019 at 23:26):will now be helping out merging PRs to the Coq OPAM archive. This means I can have quick turnaround time for Coq-community packages
Karl Palmskog (May 03 2019 at 23:26):I think I will start out by adding dev packages for all Coq-community packages that use the template
Théo Zimmermann (May 04 2019 at 10:37)::+1:
Karl Palmskog (May 15 2019 at 22:45):is there a way to test w/ 8.10 branch and/or beta in Nix?
Karl Palmskog (May 16 2019 at 01:08):ah, saw at least how to do the 8.10 branch
Karl Palmskog (May 17 2019 at 02:04):I did all the releases and package submissions for the projects I maintain, was fairly quick
Karl Palmskog (May 17 2019 at 20:19):@Théo Zimmermann do you think Hugo minds if I do releases of Stalmarck and Binary Rationals?
Karl Palmskog (May 17 2019 at 20:20):would be useful for us to get them "timestamped"
Théo Zimmermann (May 18 2019 at 14:50):I don't think he would mind.
Théo Zimmermann (May 18 2019 at 14:56):Coq 8.10+beta1 is in nixpkgs master but not yet in nixpkgs-unstable (there is always some lag). Testing with this version thus requires some waiting, or some nixpkgs pinning.
Karl Palmskog (May 18 2019 at 15:33):OK, I'll make do with v8.10 in Nix for now
Théo Zimmermann (May 22 2019 at 18:39):FWIW 8.10+beta1 is in nixpkgs-unstable now.
Karl Palmskog (May 22 2019 at 18:45):@Théo Zimmermann so this mean I can just use8.10+beta1 in meta.yml?
Théo Zimmermann (May 22 2019 at 18:58):@Karl Palmskog Put just "8.10". The Nix file converts this into coq_8_10 which is the attribute name of the package.
Karl Palmskog (May 22 2019 at 19:12):OK great
Karl Palmskog (May 22 2019 at 19:13):now I just need 8.10 Docker image and my life would be (nearly) complete
Théo Zimmermann (May 22 2019 at 19:13):Yep, waiting on @Erik Martin-Dorel for this. He might be on vacation, because otherwise he is usually pretty reactive.
Karl Palmskog (May 22 2019 at 19:16):I realized that the template should support n Coq projects instead of just 1 + extraction, have had several projects where this makes sense
Théo Zimmermann (May 22 2019 at 19:16):Yes, I think Dune in particular is going to make it easier to move towards monorepo where it makes sense.
Karl Palmskog (May 22 2019 at 19:17):it would probably be something like 1 primary + n secondary + m extraction
Théo Zimmermann (May 22 2019 at 19:17):I have an example in mind which is coq-community projects zorns-lemma + topology
Karl Palmskog (May 22 2019 at 19:18):yeah we should fix those templates to at least be up to date first though
Théo Zimmermann (May 22 2019 at 19:18):I had a PR opened about this
Théo Zimmermann (May 22 2019 at 19:18):two actually, although I think one of them needed some changes
Théo Zimmermann (May 22 2019 at 19:19):But the difference between having several projects in a monorepo and the extraction question is that in the first case the sources will be usually be located in different sub-directories
Karl Palmskog (May 22 2019 at 19:19):I think that can happen with extraction as well
Théo Zimmermann (May 22 2019 at 19:20):Right, you could have additional OCaml sources, and consider the Coq project to be a dependency.
Karl Palmskog (May 22 2019 at 19:20):I think we can write some wiki page about: the possibilities for organizing a Coq+OCaml project
Théo Zimmermann (May 22 2019 at 19:20):That would be a good step forward indeed.
Karl Palmskog (May 22 2019 at 19:21):figuring out boilerplate has taken me huge effort over time
Théo Zimmermann (May 22 2019 at 19:21):Yep, and everyone has to figure the same thing over and over
Karl Palmskog (May 22 2019 at 19:21):I remember when Ruby on Rails came around and it was "convention over configuration", they had set a lot of defaults like directory structure for you
Karl Palmskog (May 22 2019 at 19:22):it was nearly always possible to override the "biased" defaults
Théo Zimmermann (May 22 2019 at 19:22):That's what Dune has tried to do with the OCaml ecosystem as well I think. And that was indeed one of my goals with the coq-community templates ;-)
Karl Palmskog (May 22 2019 at 19:22):but you had to be sufficiently bothered by them
Karl Palmskog (May 22 2019 at 19:23):yeah I saw that they're merging dune-release into dune, that's very Rails-y
Théo Zimmermann (May 22 2019 at 19:24):Are they?
Karl Palmskog (May 22 2019 at 19:25):https://github.com/ocaml/dune/issues/2171
Karl Palmskog (May 22 2019 at 19:25):btw @Théo Zimmermann I tried getting in touch with Tej Chajed over a release of ATBR for 8.9, but no response so far, maybe we can just add me as ATBR maintainer...
Karl Palmskog (May 22 2019 at 19:27):or what do you think?
Théo Zimmermann (May 22 2019 at 19:27):How did you try to get in touch? I'm not surprised that Tej is not releasing, because he doesn't use opam, so it would make sense for you to take over the releases.
Karl Palmskog (May 22 2019 at 19:28):tried over Gitter (I think he was active recently), but I guess I can do mail as well
Théo Zimmermann (May 22 2019 at 19:28):Or issue?
Théo Zimmermann (May 22 2019 at 19:29):I wouldn't mind adding you as a maintainer there as well, however we must be careful not to make coq-community be another coq-contribs where you are the new @Hugo Herbelin. It's important that we manage to involve as many maintainers as possible in the process.
Théo Zimmermann (May 22 2019 at 19:29):We can discuss about the right strategy for this in Sophia I guess.
Karl Palmskog (May 22 2019 at 19:30):agree
Karl Palmskog (May 22 2019 at 19:33):in this case we forked all these projects (minus chapar) internally and fixed them up a bit (so we can claim this as contribution)
Karl Palmskog (May 22 2019 at 19:34):other stuff that came out of mutation work: https://github.com/math-comp/math-comp/pull/346
Karl Palmskog (May 22 2019 at 19:35):I have an absurdly long PDF (25+ pages) going through live mutants
Théo Zimmermann (May 22 2019 at 19:36):?
Karl Palmskog (May 22 2019 at 19:36):reviewers didn't think mutation itself was good enough, we have to find a bunch of weak specs as well
Karl Palmskog (May 22 2019 at 19:37):so I did a paper appendix looking at 30+ live mutants and why they are live (credit also to Emilio for many of the MathComp ones)
Théo Zimmermann (May 22 2019 at 19:38):sorry I'm a bit unclear on the terminology
Théo Zimmermann (May 22 2019 at 19:38):what do you call a "live mutant" again?
Karl Palmskog (May 22 2019 at 19:38):killed mutant: a project is modified and some proof fails
Karl Palmskog (May 22 2019 at 19:38):live mutant: a project is modified and all proofs pass
Karl Palmskog (May 22 2019 at 19:39):if you look at the MathComp PR it describes a live mutant which preserved correctness of sorting, but where complexity became O(n^2) instead of O(nlogn)
Karl Palmskog (May 22 2019 at 19:40):the added lemma would "catch" this change, since it talks about the salient non-functional property of the sort
Théo Zimmermann (May 22 2019 at 19:41):Was this issue fixed in the meantime? The PR content does not make it obvious that this is the purpose of this change.
Karl Palmskog (May 22 2019 at 19:42):we can't advertise widely since we're in double-blind review
Karl Palmskog (May 22 2019 at 19:43):we explained to Georges in an email, so he knows
Théo Zimmermann (May 22 2019 at 19:43):oh well...
Théo Zimmermann (May 22 2019 at 19:43):double-blind... sigh!
Karl Palmskog (May 22 2019 at 19:43):I'm going to implement his suggestions and we can claim "PR accepted" and so on
Karl Palmskog (May 22 2019 at 19:44):yeah, people reporting bugs are hardest hit
Karl Palmskog (May 22 2019 at 19:44):some have to use dummy GitHub accounts
Karl Palmskog (May 22 2019 at 19:44):then you get a silly line in your CV: I reported 100+ bugs/issues using these dummy accounts due to double-blind
Théo Zimmermann (May 22 2019 at 19:44):I submitted a paper in double-blind where I claim to be responsible for the Coq bug tracker migration.
Théo Zimmermann (May 22 2019 at 19:45):If people look for who did this migration, they can find out.
Théo Zimmermann (May 22 2019 at 19:45):But still the committees of two conferences did not complain.
Karl Palmskog (May 22 2019 at 19:46):yes, it's a gray area
Théo Zimmermann (May 22 2019 at 19:46):But I don't encourage people to go and see the Coq repository in my paper.
Théo Zimmermann (May 22 2019 at 19:46):So if people do, it's their fault.
Théo Zimmermann (May 22 2019 at 19:46):Previous versions of my paper were also on HAL anyway.
Karl Palmskog (May 22 2019 at 19:46):some PC chairs would not be content with that...
Karl Palmskog (May 22 2019 at 19:47):but you never know
Théo Zimmermann (May 22 2019 at 19:47):with which part?
Karl Palmskog (May 22 2019 at 19:47):referencing a repo that can be used to find out identities
Théo Zimmermann (May 22 2019 at 19:48):well, it was either this or not being able to write the paper the way I did, which would have been very unfortunate
Théo Zimmermann (May 22 2019 at 19:48):and if reviewers are looking too much, they can find out identities for sure
Théo Zimmermann (May 22 2019 at 19:49):And I provided my full analysis pipeline and the data, so I couldn't mask the repo's URL anyway
Karl Palmskog (Jul 12 2019 at 17:32):I think we may need some dictionary, "principal maintainer" vs. "Coq-community maintainer"
Karl Palmskog (Jul 12 2019 at 17:35):@Anton Trunov should we start a Coq-community issue for moving the existing awesome-coq and try to reach the owner of that repo?
Karl Palmskog (Jul 12 2019 at 17:36):I guess the opposite order may be preferred
Théo Zimmermann (Jul 12 2019 at 18:24):"principal maintainer" vs. "Coq-community maintainer"
The two mean the same to me. Do you want me to always use "Coq-community maintainer" instead of "principal maintainer"?
Karl Palmskog (Jul 12 2019 at 18:57):but I thought we were considering all Coq-community organization members as "potential maintainers" for all projects?
Karl Palmskog (Jul 12 2019 at 18:58):what would we call such non-principal maintainers for precision?
Théo Zimmermann (Jul 12 2019 at 19:37):What about just "coq-community members"? See also coq-community/manifesto#77.
Anton Trunov (Jul 13 2019 at 09:09):@Karl Palmskog I think Théo already CCed them in that issue. Still I think we should open an issue and if they aren’t resonsive we can start a new project
Karl Palmskog (Jul 13 2019 at 16:20):@Anton Trunov OK I guess we'll wait a few days more then
Anton Trunov (Jul 14 2019 at 11:49):Hi folks, has anyone tried https://reviewable.io? I hear it’s strictly more superior than the default GitHub code review interface. Could you please share your opinion on the tool?
Karl Palmskog (Aug 10 2019 at 04:11):this is something we should try to support via templates: https://github.blog/2019-08-08-github-actions-now-supports-ci-cd/
Théo Zimmermann (Aug 10 2019 at 12:53):Sure that would be nice. I have already made coq and coq-community part of the beta of GitHub Actions so this is doable as of today. Of course, before actually adding this to the templates, we should test it on an example project to ensure that it works well.
Karl Palmskog (Aug 15 2019 at 18:33):oh man, would love to try out the GitHub Actions thing out right now, but just swamped with other work
Karl Palmskog (Aug 15 2019 at 18:33):will just create an issue to collect links and resources
Anton Trunov (Aug 21 2019 at 16:30):@Théo Zimmermann @Karl Palmskog Would you mind if I added some new tags like type: library, type: plugin or something like this? I will likely get an intern or two to work on coq-community projects by the end of September. And I’d like them to choose some Coq libraries to revive, but not plugins, because it’s much harder for newcomers
Anton Trunov (Aug 21 2019 at 16:32):The new tags are supposed to further classify the coq-community/manifesto issues with maintainer-wanted tag
Anton Trunov (Aug 21 2019 at 16:32):And perhaps extraction tag could be added as well
Karl Palmskog (Aug 21 2019 at 17:13):@Anton Trunov I'm assuming this is tags for manifesto issues? Those sound good to me, but maybe something like coq-plugin coq-libraryor even external-tool for proviola etc.
Anton Trunov (Aug 21 2019 at 17:14):That’s correct, it’s for manifesto repository.
Karl Palmskog (Aug 21 2019 at 17:14):in any case, it would be good if we invented tags so that all move-project have one tag.
Anton Trunov (Aug 21 2019 at 17:15):OK, I’ll add the tags you suggested. Thanks
Anton Trunov (Aug 21 2019 at 17:15):in any case, it would be good if we invented tags so that all
move-projecthave one tag.
could you expand a bit on this?
Karl Palmskog (Aug 21 2019 at 17:17):I just meant that it would be good to invent tags so that all current projects are tagged
Karl Palmskog (Aug 21 2019 at 17:17):since we have like a bunch of them
Anton Trunov (Aug 21 2019 at 17:18):you mean in addition to move-project, right?
Karl Palmskog (Aug 21 2019 at 17:19):yes
Karl Palmskog (Aug 21 2019 at 17:19):or do you mean we replace move-project with move-coq-plugin, etc.?
Anton Trunov (Aug 21 2019 at 17:19):hmmm, now you got me thinking
Anton Trunov (Aug 21 2019 at 17:20):https://github.com/coq-community/manifesto/labels/maintainer-wanted
Anton Trunov (Aug 21 2019 at 17:20):I started adding more labels
Anton Trunov (Aug 21 2019 at 17:20):but we can change that
Karl Palmskog (Aug 21 2019 at 17:20):I think what you've added there works well
Karl Palmskog (Aug 21 2019 at 17:21):but just that we can complete the tagging for all of of those, inventing more tags if necessary
Anton Trunov (Aug 21 2019 at 17:27):ok, I added some more tags to accompany move-project, except for VsCoq
Anton Trunov (Aug 21 2019 at 17:27):coq-ide or just external-tool (or both)?
Karl Palmskog (Aug 21 2019 at 17:28):maybe just external-tool for now
Anton Trunov (Aug 21 2019 at 17:28):oops, I forgot to clear is: open
Karl Palmskog (Aug 21 2019 at 17:28):then you capture ProViola as well
Anton Trunov (Aug 21 2019 at 17:28):ok
Karl Palmskog (Aug 21 2019 at 17:28):we can rename later
Anton Trunov (Aug 21 2019 at 17:33):ok, I’m done this time, feel free to make edits
Théo Zimmermann (Aug 22 2019 at 09:12):Good job! I think I liked the idea of prefixing all this labels with type: so that it is clearer that this is a single family of tag (could also use the same color), could also be project-type: to further clarify that it is not the type of the issue or any type-theoretic notion ;-)
Théo Zimmermann (Aug 22 2019 at 09:13):We should also get some other people to add projects to this list, given how all the current ones were added by Karl.
Anton Trunov (Aug 22 2019 at 09:28):@Théo Zimmermann Having added the tags, I’m not sure type: … is the way to go. That’s because for some project we will have several type: tags. Which may be confusing since type: kind of suggests mutual exclusiveness. That said, I don’t have a strong opinion on this.
Maxime Dénès (Aug 30 2019 at 07:51):@Théo Zimmermann is it ok if I create a coq-community/vscoq gitter room?
Théo Zimmermann (Aug 30 2019 at 08:36):@Maxime Dénès For sure!
Théo Zimmermann (Aug 30 2019 at 08:38):Although that would have also been totally fine to use the main room for vscoq-specific discussions.
Maxime Dénès (Aug 30 2019 at 09:28):yeah but gitter's search is not great, so if I miss some messages, it will be easier to lookup conversations in a specific room
Théo Zimmermann (Aug 30 2019 at 11:25):indeed
Karl Palmskog (Sep 03 2019 at 02:30):a friend told me about how someone tried to socially engineer their way into being admin of one of his JavaScript GitHub repos (that a bunch of other reasonably widely used packages depended on)
Karl Palmskog (Sep 03 2019 at 02:31):as soon as he asked for LinkedIn profile and code examples the guy went silent
Karl Palmskog (Sep 03 2019 at 03:00):some vetting process for changing maintainers of more "important" Coq-community projects may be called for
Théo Zimmermann (Sep 03 2019 at 07:03):Sure, I would definitely like to make progress on this issue. Sometimes, this social engineering hacking works: you may have heard of the event-stream incident (https://blog.logrocket.com/the-latest-npm-breach-or-is-it-a427617a4185/). I can't find it now but some community organization is the JS world ceased activity because of such concerns (which are much more prevalent in their ecosystem).
Théo Zimmermann (Sep 03 2019 at 07:04):The idea of asking for another social media profile is a good one. What we could do would be to require that coq-community members have a keybase.io profile, with other social profiles beyond just GitHub.
Théo Zimmermann (Sep 03 2019 at 07:16):Although that might not work for everyone (not everyone has several social media profiles). Traditional web-of-trust is also a good solution for people that can be met at conferences or workshops.
Karl Palmskog (Sep 03 2019 at 09:52):Keybase sounds like a good start, let's discuss in the near future
Théo Zimmermann (Sep 07 2019 at 08:49):Here was the community organization I was talking about: https://github.com/electron-userland/welcome/issues/9#issuecomment-503768955
Karl Palmskog (Sep 07 2019 at 09:03):I think JavaScript communities are quite a lot looser, which makes it more of an issue for them. Coq and Isabelle/HOL communities are somewhat unique in that many core contributors have similar academic backgrounds and regularly meet at conferences. The question may be mostly in having an onboarding process for junior contributors, students, interns, etc.
Théo Zimmermann (Sep 19 2019 at 16:00):Should we propose a badge that can be added to unmaintained projects whose author agreed to move to coq-community (that have a corresponding issue in the manifesto) but which didn't find a maintainer yet? Something like that: https://img.shields.io/badge/maintainer%20wanted-on%20coq--community-%23c1272d
Anton Trunov (Sep 19 2019 at 16:02):Great idea! I hope the authors of unmaintained projecs will agree to merge such PRs :)
Karl Palmskog (Oct 08 2019 at 20:46):@Théo Zimmermann do you think Pierre and Yves mind if I do a GitHub release for CoqArt repo? I think a tag at least is needed now that changes need to be made for 8.10
Théo Zimmermann (Oct 08 2019 at 21:29):I don't think they would mind, no.
Gregory Malecha (Oct 16 2019 at 14:27):question about best practices. In the "old days" the common practice was to put .v files in a theories directory and build it with a prefix, i.e. -Q theories ProjectName (capitalization aside). However, this doesn't work well with COQPATH because with COQPATH you can only get naming structure from directories. I've seen a few projects move to a model where theories is renamed to ProjectName to address this, is this a good way to go?
Théo Zimmermann (Oct 16 2019 at 17:26):This works with COQPATH only as long as you install (which you can do in a local directory if you don't want to do this globally).
Gregory Malecha (Oct 16 2019 at 17:27):i see, so the idea is to install to a directory that is not user-contrib. is there a way to set that?
Gregory Malecha (Oct 16 2019 at 17:27):make INSTALLDIR=?
Gregory Malecha (Oct 16 2019 at 17:27):or something like that
Théo Zimmermann (Oct 17 2019 at 08:18):Something like that indeed. I don't remember if INSTALLDIR is supported. One would have to test or check the generated makefile. DESTDIR might also work. In any case, that's probably an issue that coq_makefile's documentation doesn't mention this.
Karl Palmskog (Nov 04 2019 at 17:12):this is probably something that we should do in all Coq-community projects (include explicit version in opam file): https://github.com/coq/coq/pull/11038
Guillaume Claret (Gitter import) (Nov 05 2019 at 09:39)::+1:
Anton Trunov (Dec 07 2019 at 19:19):Does anyone know why recently builds on coq-on-cachix fail?
Anton Trunov (Dec 07 2019 at 19:19): Anton Trunov (Dec 07 2019 at 19:20):opam builds on the other hand succeed
Karl Palmskog (Dec 07 2019 at 19:22):there's something wrong with ssreflect and Nix
Karl Palmskog (Dec 07 2019 at 19:22):on 8.11 and master, but not 8.10
Karl Palmskog (Dec 07 2019 at 19:22):I have no idea why
Karl Palmskog (Dec 07 2019 at 19:23):building '/nix/store/lsfra14m6kx9vrqv25y5y8ymci5q7cab-coq-8.11-git-ssreflect-dev.drv'...
/nix/store/7g6xj1kz46s8czlfkxfxc0zby8dvigsf-ocaml-findlib-1.8.1/nix-support/setup-hook: line 9: createFindlibDestdir: unbound variable
builder for '/nix/store/lsfra14m6kx9vrqv25y5y8ymci5q7cab-coq-8.11-git-ssreflect-dev.drv' failed with exit code 1
yeah, me neither
Karl Palmskog (Dec 07 2019 at 19:33):@Anton Trunov btw, any 1.10 release of fcsl-pcm in the works?
Karl Palmskog (Dec 07 2019 at 19:34):it's going to be compatibility-breaking, right? No Coq 8.9?
Anton Trunov (Dec 07 2019 at 19:34):oh yeah, I’ll try to do it later next week
Karl Palmskog (Dec 07 2019 at 19:40):@Anton Trunov I'm going to do a release of lemma-overloading for consistency (after testing 8.11 locally)
Anton Trunov (Dec 07 2019 at 19:41)::thumbsup:
Karl Palmskog (Dec 09 2019 at 15:48):repost about Lean and Coq: "There's this other system called Coq [...] It's an old version, it's the same type theory as Lean, but, you know, with more design errors" (https://www.youtube.com/watch?v=Dp-mQ3HxgDE&t=2308) (edited) "Lean is the only viable tool currently [to formalize a large part of math]" (https://youtu.be/Dp-mQ3HxgDE?t=3444)
Gregory Malecha (Dec 11 2019 at 20:30):@Karl Palmskog it sounds like we just need quotients, then all is easy :-)
Karl Palmskog (Dec 13 2019 at 09:21):if only
Karl Palmskog (Dec 27 2019 at 15:14):I set up a workflow for generating websites and coqdoc based on coqdocjs, example: https://coq-community.github.io/huffman/
Karl Palmskog (Dec 27 2019 at 15:20):structure shamelessly borrowed from MathComp
Anton Trunov (Dec 27 2019 at 16:44):@Karl Palmskog Looks awesome! Is there any documentation describing the workflow?
Karl Palmskog (Dec 27 2019 at 16:53):@Anton Trunov not yet, working on it, will probably be documented in the wiki
Anton Trunov (Dec 27 2019 at 16:54):cool! you mean the manifesto wiki, right?
Karl Palmskog (Dec 27 2019 at 16:54):right
Théo Zimmermann (Dec 27 2019 at 17:08):That's awesome @Karl Palmskog! I am a bit surprised though to see proof scripts in the coqdoc output. Is this the default behavior?
Karl Palmskog (Dec 27 2019 at 17:09):the proof scripts are for things ending in Defined, since in Huffman those don't have Proof. (which determines the hiding)
Karl Palmskog (Dec 27 2019 at 17:10):my friend is helping out with fixing some annoying things about coqdocjs
Karl Palmskog (Dec 27 2019 at 17:10):so the website will probably improve in a few hours
Théo Zimmermann (Dec 27 2019 at 17:10)::+1:
Guillaume Claret (Gitter import) (Dec 27 2019 at 17:46)::+1:
Karl Palmskog (Dec 27 2019 at 18:24):ah, now you can see some improvements here: https://coq-community.github.io/huffman/Huffman.BTree.html
Karl Palmskog (Dec 27 2019 at 18:24):spacing between lemmas looks better and I added the missing Proof. for Defined stuff
Karl Palmskog (Dec 27 2019 at 18:27):good enough to implement for lemma-overloading etc., or what do you think @Anton Trunov ?
Anton Trunov (Dec 27 2019 at 18:35):@Karl Palmskog I think so. Btw, it would be great to have deployment automated.
Karl Palmskog (Dec 27 2019 at 18:42):not sure we can conveniently automate more than GitHub does, i.e., someone has to push to the docs directory and GitHub handles it from there
Karl Palmskog (Dec 27 2019 at 18:43):in any case, the README here gives the general idea for the workflow, and I added the template index.md.mustache to the templates repo: https://github.com/palmskog/coqdocjs#usage https://github.com/coq-community/templates/blob/master/index.md.mustache
Théo Zimmermann (Dec 27 2019 at 20:02):@Karl Palmskog Can't you move the "Other related publications, if any, are listed below." inside the {{# publications }} to make it appear only if there are some publications?
Karl Palmskog (Dec 27 2019 at 20:24):@Théo Zimmermann the problem is that anything inside {{# publications}} will be repeated for every entry in the publications list
Karl Palmskog (Dec 27 2019 at 20:24):I'm sure there is a solution to this somewhere, but it's above my threshold for now
Karl Palmskog (Dec 27 2019 at 20:41):woah, glad I convinced Laurent Thery to put the Huffman pdf on HAL, his old website for the project is apparently gone now
Karl Palmskog (Jan 01 2020 at 13:37):@Théo Zimmermann so I forked CoqdocJS (https://github.com/tebbi/coqdocjs) and modified it with the help of a friend for documentation in Coq-community projects: https://github.com/palmskog/coqdocjs
Karl Palmskog (Jan 01 2020 at 13:38):ideally the changes could be contributed upstream, but the median waiting time to merge a PR there seems to be 8+ months
Karl Palmskog (Jan 01 2020 at 13:39):what do you think about a specialized fork living in the coq-community org, e.g., coqdocjs-community?
Karl Palmskog (Jan 01 2020 at 13:39):we could try to contribute stuff upstream but not be dependent on it
Théo Zimmermann (Jan 02 2020 at 09:28):Sorry if I'm asking the obvious, but wouldn't another option be to propose the transfer of coqdocjs to coq-community? @tebbi could still be one of the maintainers, but other people (like you and your friend) could help make it more actively maintained...
Karl Palmskog (Jan 02 2020 at 09:36):@Théo Zimmermann I considered this, but there are a number of adaptations that only make sense for coq-community or similar
Karl Palmskog (Jan 02 2020 at 09:37):for example, footer links to coq-community, Makefile tasks assume one follows conventions
Karl Palmskog (Jan 02 2020 at 09:38):and instructions are getting quite non-general at this point (assumes GitHub pages are used)
Karl Palmskog (Jan 02 2020 at 09:38):I guess I could start an issue and ask tebbi what he prefers
Théo Zimmermann (Jan 02 2020 at 09:39):OK I see. Are these additions easy to maintain on top of coqdocjs? Not that it is likely to evolve much...
Karl Palmskog (Jan 02 2020 at 09:40):well, the core scripts are essentially the same (although that may change)
Karl Palmskog (Jan 02 2020 at 09:41):but basically everything else is different
Karl Palmskog (Jan 02 2020 at 09:41):so it will be quite a hassle to maintain on top of existing coqdocjs
Karl Palmskog (Jan 02 2020 at 09:42):the proposal was to be a good citizen and contribute general improvements upstream separately, but specialize in the repo
Théo Zimmermann (Jan 02 2020 at 09:44):OK... Sometimes, the good way of making such specialization possible is to use optional switches and flags. So that if the version of coqdocjs that is used in coq-community continues to receive improvements, everyone in the community can benefit. So that anyone wanting to host documentation for a Coq project on GitHub pages can use the additional feature without being constrained by the rest, etc. But this may represent additional work...
Karl Palmskog (Jan 02 2020 at 09:45):too much work for me, this is already way over my time budget
Théo Zimmermann (Jan 02 2020 at 09:46):Right. Well opening an issue to discuss it seems like a good option. It could be an issue in coq-community/manifesto where you mention tebbi so that other persons from the community see it too. So people may have the time that you lack to complete what you started...
Karl Palmskog (Jan 02 2020 at 09:51)::thumbsup:
Karl Palmskog (Jan 02 2020 at 10:21):ok done as coq-community/manifesto#88
Karl Palmskog (Jan 02 2020 at 12:38):@Anton Trunov we should do an attempt on the awesome-coq thing again, the OCaml version has almost 2000 stars: https://github.com/ocaml-community/awesome-ocaml
Karl Palmskog (Jan 02 2020 at 12:41):I might start one for HOL4 just for fun
Karl Palmskog (Jan 04 2020 at 20:30):https://github.com/coq-community/manifesto/wiki/Generating-and-deploying-coqdoc-HTML-documentation
Anton Trunov (Jan 04 2020 at 20:56):we should do an attempt on the awesome-coq thing again, the OCaml version has almost 2000 stars
Anton Trunov (Jan 04 2020 at 20:57):@Karl Palmskog Right, maybe we should just start. I’ll try to put some of my personal notes somewhere (most likely this week).
Anton Trunov (Jan 04 2020 at 20:58):I might start one for HOL4 just for fun
If you started this one, could you please share the link?
Anton Trunov (Jan 04 2020 at 20:58):And kudos for documenting how to use coqdoc!
Karl Palmskog (Jan 04 2020 at 20:59):maybe one try to ping the other guy doing awesome-coq in his own account
Karl Palmskog (Jan 04 2020 at 21:01):coqdoc can do nice stuff but it's arguably undermaintained
Karl Palmskog (Jan 04 2020 at 21:01):for example I reported the serious bug which makes all sentences with annotations disappear
Anton Trunov (Jan 04 2020 at 21:09):maybe one try to ping the other guy doing awesome-coq in his own account
oh, you think they didn’t get a notification because we mentioned the organization, not their personal account? then we should try pinging them at least one more time
Anton Trunov (Jan 04 2020 at 21:11):I guess we should ask then if the repo owner would like to transfer the repo under coq-community and become a maintainer?
Anton Trunov (Jan 04 2020 at 21:13):@Théo Zimmermann @Karl Palmskog what do you think?
Karl Palmskog (Jan 04 2020 at 21:14):right, we can try opening an issue in his repo, if no response in a couple of days then we plow ahead
Anton Trunov (Jan 04 2020 at 21:24):ok, here is the issue https://github.com/uhub/awesome-coq/issues/11
Karl Palmskog (Jan 04 2020 at 21:35)::thumbsup:
Karl Palmskog (Jan 04 2020 at 21:38):the main drawback with that collection is that it seems to be only Coq projects, not books, tools connected to Coq, etc.
Anton Trunov (Jan 04 2020 at 21:38):I’ve noticed Programs and Proofs by I. Sergey there
Karl Palmskog (Jan 04 2020 at 21:41):right, but that's arguably a Coq project too
Karl Palmskog (Jan 09 2020 at 09:48):@Anton Trunov so I think we can just go ahead and create the awesome-coq repo, I'll do it later today unless you have objections
Karl Palmskog (Jan 09 2020 at 09:48):the OCaml one is a good template
Anton Trunov (Jan 09 2020 at 10:55):@Karl Palmskog Sounds good!
Karl Palmskog (Jan 09 2020 at 11:15):the main work may be to get it listed in all other awesome lists
Anton Trunov (Jan 09 2020 at 11:16):that’s for sure the biggest challenge :)
Karl Palmskog (Jan 09 2020 at 17:51):@Anton Trunov do you think there's a chance we could get permission to use Lilia Anisimova's mechanical Coq painting for awesome-coq?
Karl Palmskog (Jan 09 2020 at 17:52):they have some nice OCaml image for awesome-ocaml, that would be a nice equivalent
Karl Palmskog (Jan 09 2020 at 19:23):this should be enough that people are annoyed their favorite project isn't listed: https://github.com/coq-community/awesome-coq
Karl Palmskog (Jan 09 2020 at 19:25):I guess I can/will also catch flak for headings/subject division
Emilio Jesús Gallego Arias (Jan 09 2020 at 20:16):very nice folks, congrats!!
Emilio Jesús Gallego Arias (Jan 09 2020 at 20:17):should it be added to Coq's README / webpage?
Karl Palmskog (Jan 09 2020 at 20:20):I think we should wait for more opinions/PRs
Karl Palmskog (Jan 09 2020 at 20:28):things feel a bit redundant in the list w.r.t. the wiki and website, but I feel it's for a good marketing cause in the end...
Karl Palmskog (Jan 09 2020 at 21:19):there should probably be a "Framework" section for Bedrock2, Fiat, Iris, Verdi, VST
Karl Palmskog (Jan 09 2020 at 21:35):and Disel, Aneris
Anton Trunov (Jan 09 2020 at 21:41):do you think there's a chance we could get permission to use Lilia Anisimova's mechanical Coq painting for awesome-coq?
Anton Trunov (Jan 09 2020 at 21:41):I can ask Ilya about that
Karl Palmskog (Jan 09 2020 at 21:42)::thumbsup:
Anton Trunov (Jan 09 2020 at 21:42):But first, do we not want to reuse coq-community’s logo?
Anton Trunov (Jan 09 2020 at 21:42):CC @Théo Zimmermann
Karl Palmskog (Jan 09 2020 at 21:42):I mean, the list is not about coq-community
Anton Trunov (Jan 09 2020 at 21:42):fair enough
Anton Trunov (Jan 09 2020 at 21:43):Let us wait for Théo’s response and if there is consensus I’ll go ahead and ask Ilya
Karl Palmskog (Jan 09 2020 at 21:43):OK
Karl Palmskog (Jan 09 2020 at 21:44):we could use the part of the coq-community logo that doesn't have text I guess
Karl Palmskog (Jan 09 2020 at 21:45):but since we hopefully will get listed in other lists, I'd try to avoid conflating coq-community with Coq in general
Anton Trunov (Jan 09 2020 at 22:17):btw, looks like awesome-ocaml reuses the OCaml logo
Karl Palmskog (Jan 09 2020 at 22:23):sure, but the Coq logo is not nice to look at
Karl Palmskog (Jan 09 2020 at 22:47):note to self: add Coq OPAM repo ref under Package Management
Théo Zimmermann (Jan 10 2020 at 09:56):What about referring back to this https://github.com/sindresorhus/awesome instead of that https://github.com/bayandin/awesome-awesomeness?
Théo Zimmermann (Jan 10 2020 at 09:57):It has always been very hard to maintain the lists on the Coq website and in the wiki, so I would be happy to refer to this list as a more exhaustive one.
Théo Zimmermann (Jan 10 2020 at 09:59):You are free to use the coq-community logo but I agree with @Karl Palmskog that it could be confusing (unless you write something like "this awesome-coq list project is part of the coq-community organization")
Théo Zimmermann (Jan 10 2020 at 10:00):It is a bit weird that "coq-community" is missing from the Community section...
Théo Zimmermann (Jan 10 2020 at 10:02):Discourse is as much official as Coq-Club FTR, and Gitter as well. However, I would add some description so that people do not confuse the purpose of Gitter and Discourse / Coq-Club: Gitter is more for questions about the development of Coq and plugins and less appropriate for beginners' questions (even if we are nice).
Théo Zimmermann (Jan 10 2020 at 10:03):There is also a non-official IRC
Théo Zimmermann (Jan 10 2020 at 10:03):And linking to Stack Overflow / Exchange could make sense as well since there is a growing community there.
Théo Zimmermann (Jan 10 2020 at 10:05):The user interface section is missing lots: cf. my wip PR https://github.com/coq/www/pull/128 (I should have finished this long ago)
Théo Zimmermann (Jan 10 2020 at 10:07):I feel this is missing a "Verified Libraries" section.
Théo Zimmermann (Jan 10 2020 at 10:09):And of course, the "Plugins" part should list Equations at the very least (but probably also QuickChick, etc.). A good list to inspire from is the one in Coq's CI: https://gitlab.com/coq/coq/pipelines/108285091
Théo Zimmermann (Jan 10 2020 at 10:09):And UniMath should be listed in the "Mathematics" section.
Karl Palmskog (Jan 10 2020 at 10:27):many points raised above are fixed by Anton's PR which I'll merge very soon
Karl Palmskog (Jan 10 2020 at 10:27):.
Karl Palmskog (Jan 10 2020 at 12:56):@Anton Trunov I did another pass on the list. We may want to consider a top-level division into "Projects" and "Resources", like they have for Java and many others: https://raw.githubusercontent.com/akullpp/awesome-java/master/README.md
Anton Trunov (Jan 10 2020 at 13:25):@Karl Palmskog looks awesome :)
Karl Palmskog (Jan 10 2020 at 13:32):@Anton Trunov so the recommended license is CC0, is that OK with you? https://creativecommons.org/publicdomain/zero/1.0/
Emilio Jesús Gallego Arias (Jan 10 2020 at 19:49):@Anton Trunov I was going to tweet about https://github.com/coq-community/awesome-coq but maybe you want to do it instead?
Karl Palmskog (Jan 10 2020 at 19:52):I have some changes standing by until Anton confirms the license.
Karl Palmskog (Jan 10 2020 at 19:53):so please don't tweet just yet
Emilio Jesús Gallego Arias (Jan 10 2020 at 19:57):Twitter is a wild place tho :)
Karl Palmskog (Jan 10 2020 at 19:58):if I start using it, I'm sure there will be some army of nitpickers looking at who you're retweeting, typos, etc.
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:00):it depends on your "community"
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:00):for me it is by far the preferred professional network these days
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:00):I was kinda joking about the wild place
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:01):something tweeter exceeds at is "I write this amazing piece of software/blog, I get 2 RT"
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:01):"some random folk sees my piece, posts it, gets 100K RTs"
Karl Palmskog (Jan 10 2020 at 20:01):personally I don't like the mix of professional and politics
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:01):xD
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:01):Ah, politics.
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:02):yeah, the mix is a problem
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:02):somehow my stream looks pretty good tho
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:02):I get the occasional politics things, but mostly about interesting CS stuff
Karl Palmskog (Jan 10 2020 at 20:03):you see someone you respect professionally, and then find out viewpoint differences are fundamental and irreconcilable
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:03):but that has happened in other social networks I was such as FB or G+
Karl Palmskog (Jan 10 2020 at 20:03):ignorance is bliss in most cases
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:04):even people using twitter for 100% technical topics have to write about other stuff ; tho I don't care so much on the case you point out, I guess I try to separate
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:04):overall far from perfect but I get a positive return from twitter
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:05):on the other hand I'm unsure research is not a lot about politics, stuff such as open source, open access, etc...
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:05):are pretty much a political aspect of my professional job
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:05):and many other stuff I'll skip but relevant to France
Karl Palmskog (Jan 10 2020 at 20:05):this is not where people usually stay
Karl Palmskog (Jan 10 2020 at 20:06):if it was mostly about open source/access, it'd be fine
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:06):I used to say that universities are just advanced training camps for politicians
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:06):well that's just an example
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:06):of course things can go further beyond
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:06):on the other hand isn't it working as intended?
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:07):if you get information on twitter that you may have a problem with certain person, isn't it an efficiency improvement?
Karl Palmskog (Jan 10 2020 at 20:07):not the right forum here for discussing this, but let's just say I disagree fundamentally with how Twitter is run as a platform
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:10):indeed, sorry for the noise; as I said I like it because lots of people is there and my S/N ratio is pretty high; on the other hand discussion about social media platform may be on topic for this channel. For example having a coq-community twitter account could be actually very very good.
Just out of curiosity, is there any other professional social network that you find interesting?
Karl Palmskog (Jan 10 2020 at 20:13):hmm, I don't think there is
Karl Palmskog (Jan 10 2020 at 20:13):I'd prefer some kind of decentralized, crypto-based stuff
Emilio Jesús Gallego Arias (Jan 10 2020 at 20:14):that'd be cool, however there are problems for those to scale, in particular w.r.t. to blocking etc... which sadly seem to be a very real issue in the real world
Karl Palmskog (Jan 10 2020 at 20:22):at least if one can do broadcast crypto you can control who gets to read something
Anton Trunov (Jan 10 2020 at 20:48):@Karl Palmskog CC0 is the perfect license. I’m happy we are on the same page here :)
Karl Palmskog (Jan 10 2020 at 20:49)::thumbsup:
Anton Trunov (Jan 10 2020 at 20:50):@Emilio Jesús Gallego Arias Sure, feel free to tweet, I’ll retweet it :) But, perhaps, we should let the list become a bit more mature. I’d like to add some more stuff from Deepspec and from Coq’s CI too
Karl Palmskog (Jan 10 2020 at 20:50):OK I pushed a version with LICENSE and stuff
Karl Palmskog (Jan 10 2020 at 20:51):can for sure be tweeted out
Anton Trunov (Jan 10 2020 at 20:51):Oh, I just saw your twitter issue. I think it could be better to tweet it from the coq-community account
Karl Palmskog (Jan 10 2020 at 20:53):do we have a coq-community twitter? news to me...
Karl Palmskog (Jan 10 2020 at 20:53):ah didn't see issue
Karl Palmskog (Jan 10 2020 at 21:25):hmm, having a logo is a requirement for getting into the main "awesome"
Karl Palmskog (Jan 10 2020 at 21:28):however, my editing skills are crap, so maybe someone can take the coq-community svg and remove the text and produce some logo like here: https://github.com/sindresorhus/awesome-electron/blob/master/readme.md
Anton Trunov (Jan 10 2020 at 21:47):@Karl Palmskog thanks for the reminder about the logo. should I ask Ilya for the logo by Lilia?
Karl Palmskog (Jan 10 2020 at 22:02):well, you can do it unless you want to try to edit the coq-community svg
Karl Palmskog (Jan 10 2020 at 22:03):I think either is fine as right aligned like the example
Karl Palmskog (Jan 11 2020 at 12:14):HoTT builds documentation for every commit, which has made their repo very inconvenient to clone
Karl Palmskog (Jan 11 2020 at 12:15):took me several minutes last time, and takes several hundred MB on disk
Karl Palmskog (Jan 11 2020 at 12:17):with in-repo generated documentation, I think the only sensible thing is to only have docs for releases, and do "one release per major Coq version"
Karl Palmskog (Jan 11 2020 at 12:19):or what do you think @Anton Trunov @Théo Zimmermann ?
Karl Palmskog (Jan 11 2020 at 12:20):for per-commit documentation, one should either use a separate repo or some service akin to readthedocs, IMO
Karl Palmskog (Jan 11 2020 at 12:21):btw @Anton Trunov do you mind if I edit your awesome-coq PR directly? Some projects arguably don't fit the list since it's supposed to be curated and about popular/unique projects
Théo Zimmermann (Jan 11 2020 at 13:30):with in-repo generated documentation, I think the only sensible thing is to only have docs for releases, and do "one release per major Coq version"
makes sense indeed
Anton Trunov (Jan 11 2020 at 14:33):@Karl Palmskog sure, feel free to edit the PR, I kind of did it mechanically to get the discussion started on what should be filtered out
Anton Trunov (Jan 12 2020 at 20:54):@Karl Palmskog Ilya Sergey has told me in private communication that we can use the "Le coq mécanisé” picture as the logo of the awesome-coq repo.
Karl Palmskog (Jan 12 2020 at 22:03)::thumbsup:
Karl Palmskog (Jan 12 2020 at 22:03):very, very nice
Karl Palmskog (Jan 12 2020 at 22:03):that painting is just an overall joy to look at
Karl Palmskog (Jan 13 2020 at 00:32):gah, I can't make Lilia's logo fit very well, due to how the awesome guidelines either require "full width" or "100px-wide"
Karl Palmskog (Jan 13 2020 at 00:33):@Anton Trunov I dabbled with Inkscape and tried the Coq-community logo, which seems to fit better: https://github.com/coq-community/awesome-coq/tree/add-svg-logo
Karl Palmskog (Jan 13 2020 at 00:33):compare: https://github.com/coq-community/awesome-coq/tree/add-logo
Karl Palmskog (Jan 13 2020 at 00:34):here's the recommended style: https://github.com/dhamaniasad/awesome-postgres/blob/master/README.md
Anton Trunov (Jan 13 2020 at 08:06):@Karl Palmskog Could you point me to the awesome guidelines? I couldn't find the requirements you pointed out. Also, I tried running awesome-lint on the project, but it fails with a syntactic error :exploding_head:
Anton Trunov (Jan 13 2020 at 08:06):thanks for your edits, btw
Karl Palmskog (Jan 13 2020 at 08:37):https://github.com/sindresorhus/awesome/blob/master/pull_request_template.md
Karl Palmskog (Jan 13 2020 at 08:37):there's a bullet about logos there
Anton Trunov (Jan 13 2020 at 09:50):Includes a project logo/illustration whenever possible.
Either centered, fullwidth, or placed at the top-right of the readme. (Example)
The image should link to the project website or any relevant website.
The image should be high-DPI. Set it to maximum half the width of the original image.
Anton Trunov (Jan 13 2020 at 09:51):looks like something like [<img src="coq-logo.png" align="right" width="10%">](https://coq.inria.fr) should work
Karl Palmskog (Jan 13 2020 at 09:51):the problem with 10% is that it can look terrible with non-svg images
Karl Palmskog (Jan 13 2020 at 09:52):depending on resolution and so on
Karl Palmskog (Jan 13 2020 at 10:01):the problem is that the painting's height makes it a hard fit for either centered or right-aligned
Anton Trunov (Jan 13 2020 at 10:10):Oh, I see. Your choice then, I have no working experience in this area :)
Karl Palmskog (Jan 13 2020 at 10:14):I'm not very experienced either, but then I would go with the .svg one for now, at least until we can consult with an expert
Karl Palmskog (Jan 13 2020 at 10:41):I think we tick all the awesome list boxes except for "30 days from creation" now
Anton Trunov (Jan 13 2020 at 10:46)::+1:
Karl Palmskog (Jan 13 2020 at 10:47):oh man I was looking up CertikOS stuff
Karl Palmskog (Jan 13 2020 at 10:47):there's basically almost nothing public anymore w.r.t. source code
Karl Palmskog (Jan 13 2020 at 10:47):if there ever was anything...
Karl Palmskog (Jan 13 2020 at 10:48):at least my view is that public source should be available...
Karl Palmskog (Jan 13 2020 at 10:51):(for addition to awesome-coq)
Anton Trunov (Jan 13 2020 at 10:53):at least my view is that public source should be available...
I can't recall them ever publishing the source code, actually
Karl Palmskog (Jan 13 2020 at 10:54):right, probably reserved for startup: https://www.certik.org/#home
Karl Palmskog (Jan 13 2020 at 10:55):what annoys me about many US academic startups: they typically get bought by some tech giant eventually, code/tech never gets used, then everything disappears in the last reorganization
Karl Palmskog (Jan 13 2020 at 10:58):founders win, almost everyone else loses
Théo Zimmermann (Jan 13 2020 at 11:43):With the way the coq-community logo is displayed now, I feel like this reinforces confusion, as clicking on the logo links to the official Coq website.
Théo Zimmermann (Jan 13 2020 at 11:44):What about making "the Coq proof assistant" a clickable link in the top description?
Théo Zimmermann (Jan 13 2020 at 12:01):OK fixed by PR!
Anton Trunov (Jan 13 2020 at 12:02)::+1:
Théo Zimmermann (Jan 13 2020 at 12:03):Regarding the order of the subsections within "Projects" I am confused. It looks almost alphabetical, but "User interfaces" is misplaced then. If it is not meant to be alphabetical, then I think that moving "Frameworks", "Libraries", "Plugins" and "Tools" closer to each other (for instance in that order) would be better.
Karl Palmskog (Jan 13 2020 at 12:05):User Interfaces is sorted under "I", as it was in the OCaml list
Karl Palmskog (Jan 13 2020 at 12:05):but feel free to call it "Interfaces" or move it to the bottom
Théo Zimmermann (Jan 13 2020 at 12:06):Ah... OK.
Théo Zimmermann (Jan 13 2020 at 12:08):Bignums is a plugin in the sense that it contains OCaml code. I guess you class it as "library" because from a user's perspective it is used as such?
Anton Trunov (Jan 13 2020 at 12:09):yeah, sometimes it’s hard to classify things, but feel free to propose changes
Théo Zimmermann (Jan 13 2020 at 12:09)::+1:
Karl Palmskog (Jan 13 2020 at 12:09):lumping vs. splitting, indeed super hard
Karl Palmskog (Jan 13 2020 at 12:10):I like the approach with tagging stuff with multiple tags, but the format here doesn't permit that
Anton Trunov (Jan 13 2020 at 12:10):I second that
Anton Trunov (Jan 13 2020 at 12:10):tagging as in org files usually works great
Théo Zimmermann (Jan 13 2020 at 12:12):Should CFML be added somewhere? Should it go into "Framework" or into "Tools"?
Anton Trunov (Jan 13 2020 at 12:12):I guess “Tools” would be better, since it’s kind of related to CoqOfOCaml
Théo Zimmermann (Jan 13 2020 at 12:13):Yeah, I was thinking the same.
Anton Trunov (Jan 13 2020 at 12:13):and yes, CFML should be added, imho
Théo Zimmermann (Jan 13 2020 at 12:13):I can open a PR for this one and Freespec too.
Anton Trunov (Jan 13 2020 at 12:14):by all means please do go ahead!
Karl Palmskog (Jan 13 2020 at 12:14):I feel CFML is more of a framework personally, but could go either way
Karl Palmskog (Jan 13 2020 at 12:15):I will probably add CoqEAL later today
Théo Zimmermann (Jan 13 2020 at 12:16):OK the authors' description are clear:
Anton Trunov (Jan 13 2020 at 12:16):btw, we are also missing Kami
Karl Palmskog (Jan 13 2020 at 12:18):is Kami maintained? last commit was like 1 year ago
Anton Trunov (Jan 13 2020 at 12:18):hmm, it feels like Kami is still a prominent Coq project
Anton Trunov (Jan 13 2020 at 12:19):but I don’t have a strong opinion about that
Karl Palmskog (Jan 13 2020 at 12:19):maybe we can check with Jason Gross, he has two open unmerged PRs
Karl Palmskog (Jan 13 2020 at 12:19):I'm personally a bit averse to listing completely abandoned projects
Anton Trunov (Jan 13 2020 at 12:36):How about these DeepSpec projects and their respective categories?
Karl Palmskog (Jan 13 2020 at 12:39):CertiCoq has not seen complete release to my knowledge
Karl Palmskog (Jan 13 2020 at 12:41):InteractionTrees is quite new, I think I'd like to see someone vouch for its uniqueness, etc.
Karl Palmskog (Jan 13 2020 at 12:41):hs-to-coq is fine
Karl Palmskog (Jan 13 2020 at 12:42):Vellvm is also a bit of a question mark, I don't see any releases except for papers, and seems stuck on Coq 8.8?
Anton Trunov (Jan 13 2020 at 12:43):hs-to-coq it is then :) thanks
Karl Palmskog (Jan 13 2020 at 12:51):I was thinking autosubst as well, but I think someone should check it actually builds on recent Coq
Karl Palmskog (Jan 13 2020 at 12:51):ah, and Metalib
Karl Palmskog (Jan 13 2020 at 12:52):both have been used in multiple papers and so on
Anton Trunov (Jan 13 2020 at 12:59):Isn’t Metalib stuck on Coq 8.6?
Karl Palmskog (Jan 13 2020 at 13:02):nope
Karl Palmskog (Jan 13 2020 at 13:03):I used it recently from GitHub
Karl Palmskog (Jan 13 2020 at 13:03):in 8.10
Anton Trunov (Jan 13 2020 at 13:03)::+1:
Anton Trunov (Jan 13 2020 at 13:08):@Karl Palmskog Are we using the alphabetical order in Tools section?
Karl Palmskog (Jan 13 2020 at 13:08):that's the intention, feel free to fix Menhir
Anton Trunov (Jan 13 2020 at 13:09):ok
Karl Palmskog (Jan 13 2020 at 13:09):some more candidates, Hahn, Coq-prelude, coq-haskell
Anton Trunov (Jan 13 2020 at 13:13):Tested hs-to-coq on Coq 8.10 and added it to the list
Anton Trunov (Jan 13 2020 at 13:59):@Karl Palmskog What do you think about jscert? It’s not that active anymore, but looks like is still maintained
Karl Palmskog (Jan 13 2020 at 14:00):I think they submitted stuff quite recently
Karl Palmskog (Jan 13 2020 at 14:00):to the OPAM archive
Anton Trunov (Jan 13 2020 at 14:00):oh, cool, hadn’t noticed that
Anton Trunov (Jan 13 2020 at 14:01):ok, let us add it then
Anton Trunov (Jan 13 2020 at 14:02):not sure about the section, though
Anton Trunov (Jan 13 2020 at 14:03):maybe “tools"?
Anton Trunov (Jan 13 2020 at 14:05):or, since they have a verified interpreter, it can go to the “Verified Software” section
Karl Palmskog (Jan 13 2020 at 14:06):it's more verified software to me
Karl Palmskog (Jan 13 2020 at 14:06):there might be a PL section at some point
Anton Trunov (Jan 13 2020 at 14:07):yep, looks like we will need a more fine-grained categorization
Anton Trunov (Jan 13 2020 at 14:26):Or even re-categorize things. Like this Tool/Plugin dichitomy sometimes creates confusion as many tools integrate with Coq as a plugin
Anton Trunov (Jan 13 2020 at 14:27):Perhaps we could re-categorize some of those by their purpose?
Anton Trunov (Jan 13 2020 at 14:28):E.g. CoqHammer could go into “Proof automation” section (and we could add SMT-Coq there too among others)
Karl Palmskog (Jan 13 2020 at 14:30):a bit too complex for me, I meant tool as in something that processes/produces something outside of Coq
Karl Palmskog (Jan 13 2020 at 14:31):I tried to follow the lead from OCaml and other awesome lists
Anton Trunov (Jan 13 2020 at 14:33):e.g. awesome-ocaml list categorizes things by “areas”: Systems programming, Testing, Concurrency, etc.
Anton Trunov (Jan 13 2020 at 14:38):speaking of SMT-Coq, I’m gonna add it if you don’t mind
Karl Palmskog (Jan 13 2020 at 14:38):sure, you can add SMT-Coq, but let's not do more categories for a little while
Anton Trunov (Jan 13 2020 at 14:38):sure, np
Karl Palmskog (Jan 13 2020 at 15:14):we should also add Mike Nahas' tutorial, which is apparently hosted in Coq's own repo
Karl Palmskog (Jan 13 2020 at 15:16):the top ones seem to be that one and Yves' Coq in a Hurry, which doesn't have source code and hasn't been updated in a while, I will shoot Yves an email and ask what the status is there
Anton Trunov (Jan 13 2020 at 15:16)::+1:
Théo Zimmermann (Jan 13 2020 at 15:45):Mike Nahas' best location to reference is https://mdnahas.github.io/doc/nahas_tutorial.html
Théo Zimmermann (Jan 13 2020 at 15:45):The one in the Coq repo has some issue and will soon redirect to the former.
Théo Zimmermann (Jan 13 2020 at 15:46):I haven't read it yet but another recent short tutorial is https://learnxinyminutes.com/docs/coq/
Karl Palmskog (Jan 13 2020 at 15:47):OK good to know
Théo Zimmermann (Jan 13 2020 at 15:48):I guess mentioning CodeWars could also make sense (https://www.codewars.com/kata/search/coq). I haven't tested it much myself though.
Karl Palmskog (Jan 13 2020 at 18:15):hmm, this is interesting, it seems SiFive has rewritten Kami: https://github.com/sifive/Kami
Anton Trunov (Jan 13 2020 at 19:35):yep, also noticed it, looks like we should add it
Karl Palmskog (Jan 25 2020 at 15:55):hmm, "interactive proof assistant"? I think we should either use simply "proof assistant" or "interactive theorem prover"
Karl Palmskog (Jan 25 2020 at 15:56):w.r.t. this: https://twitter.com/CoqLang
Emilio Jesús Gallego Arias (Jan 25 2020 at 15:57):the official denomination is "The Coq Proof Assistant"
Emilio Jesús Gallego Arias (Jan 25 2020 at 15:57):and we often use Interactive Proof Assistant
Emilio Jesús Gallego Arias (Jan 25 2020 at 15:57):I dunno, that's what the Coq project has used for a long time
Karl Palmskog (Jan 25 2020 at 15:59):"interactive theorem prover": ~250k Google hits, "proof assistant": ~220k Google hits, "interactive proof assistant": ~20k Google hits
Karl Palmskog (Jan 25 2020 at 16:01):so I would argue for one of the first two, just "Coq proof assistant" is fine...
Emilio Jesús Gallego Arias (Jan 25 2020 at 16:03):ok done!
Karl Palmskog (Jan 25 2020 at 16:04):"interactive proof assistant" is mentioned twice on the Coq website
Karl Palmskog (Jan 25 2020 at 16:05):once in the manual, once for some old workshop
Karl Palmskog (Jan 25 2020 at 16:07):it seems the manual uses it to refer to a mode of use of Coq, i.e., Coq backend + some GUI
Anton Trunov (Jan 26 2020 at 20:03):@Emilio Jesús Gallego Arias Cool background picture!
Emilio Jesús Gallego Arias (Jan 26 2020 at 22:59)::)
Emilio Jesús Gallego Arias (Jan 26 2020 at 22:59):Théo any comments on the mail I sent on twitter? (@zimmi48)
Emilio Jesús Gallego Arias (Jan 26 2020 at 23:01):@Anton Trunov will send you the stuff you requested tomorrow.
Even if the mailing list was needed as to have a "mail" for the twitter, and could be useful for other bits, maybe we should handle stuff more dynamically? Should we create a gitter account ? @Anton Trunov @Théo Zimmermann
Théo Zimmermann (Jan 27 2020 at 10:15):Why not? Sorry for not answering your e-mails faster Emilio, I've been very busy!
Karl Palmskog (Jan 27 2020 at 10:27):nitpick suggestion for Twitter description: "Coq is a general-purpose interactive theorem prover [or: "proof assistant" or: "formal proof management system"] with applications in formal mathematics and software verification"
Emilio Jesús Gallego Arias (Jan 27 2020 at 10:57):@Théo Zimmermann sorry I didn't mean to rush, I know you are very busy; I'll create a gitter room then!
Emilio Jesús Gallego Arias (Jan 27 2020 at 10:58):@Karl Palmskog indeed I'll adjust the description to what's on Coq's webpage , thanks; out of curiosity, what you have against "interactive proof assistant" :)
Karl Palmskog (Jan 27 2020 at 12:20):@Emilio Jesús Gallego Arias no general problem, just think we need to be consistent with terminology
Karl Palmskog (Jan 27 2020 at 12:21):otherwise one might get lots of questions about what is "interactive proof assistant" vs. "proof assistant"
Karl Palmskog (Jan 27 2020 at 12:21):I know at least paper reviewers complain about these things a lot...
Karl Palmskog (Jan 27 2020 at 12:22):in any case, this ties in a bit with guidelines for Coq advocacy: "[try to] use agreed-on/sanctioned terminology"
Théo Zimmermann (Jan 27 2020 at 15:28):I agree with Karl on being consistent and on ITP and "proof assistant" being standard.
Jason Gross (Jan 28 2020 at 04:57):Is someone willing to take a look at this +15,-7 change in porting a .ml4/mlg from 8.9 to 8.10? https://github.com/coq-community/reduction-effects/pull/5/files#diff-70aff75dd897e7c57305ffc170af922c (In particular, wondering if I did the right thing with global env/sigma, especially given that the deprecation message for UnivGen.type_of_global suggested using a function which doesn't actually exist (Typeops.type_of_global)
Karl Palmskog (Jan 28 2020 at 18:57):ah, I see the first tweet is out, but not all CoqPL talks are actually in the YT playlist
Karl Palmskog (Jan 28 2020 at 18:57):(not included: https://popl20.sigplan.org/details/CoqPL-2020-papers/2/The-use-of-Coq-for-Common-Criteria-Evaluations)
Anton Trunov (Jan 28 2020 at 18:58):@Karl Palmskog Any idea who we should talk to?
Karl Palmskog (Jan 28 2020 at 18:59):my guess is that they didn't want it recorded?
Anton Trunov (Jan 28 2020 at 18:59):oh, I see. I guess too late now :))
Karl Palmskog (Jan 28 2020 at 19:00):I guess so yeah, but at least wanted to point this out
Emilio Jesús Gallego Arias (Jan 28 2020 at 19:00):Ouch I only checked the last and first one so I thought
Emilio Jesús Gallego Arias (Jan 28 2020 at 19:00):it is complete
Emilio Jesús Gallego Arias (Jan 28 2020 at 19:00):not a big deal tho, if one is missing
Karl Palmskog (Jan 28 2020 at 19:01):unsound tweet :wink:
Anton Trunov (Jan 28 2020 at 19:01):hahaha
Emilio Jesús Gallego Arias (Jan 28 2020 at 19:01):XDDDD
Anton Trunov (Jan 28 2020 at 19:01):the sound of an unsound tweet
Emilio Jesús Gallego Arias (Jan 28 2020 at 19:01):twitter's logic is paraconsistent tho
Emilio Jesús Gallego Arias (Jan 28 2020 at 19:01):so we are allowed to do that
Karl Palmskog (Jan 28 2020 at 19:02):I recall the discussion on LTU on Conor McBride's PhD thesis, which claimed: John Major was the last Tory prime minister
Karl Palmskog (Jan 28 2020 at 19:02):I think Andrej Bauer (jokingly) called for a retraction of the thesis (on grounds of false claim)
Anton Trunov (Jan 28 2020 at 19:03):This should go into awesome-type-theory-jokes list
Karl Palmskog (Jan 28 2020 at 19:04):in any case, can we get a tweet of Gaëtan's announcement? maybe the Discourse link?
Karl Palmskog (Jan 28 2020 at 19:05):if there's any justice (true judgement?) it will go viral
Anton Trunov (Jan 28 2020 at 19:05):Let me qoute @Emilio Jesús Gallego Arias on this: @Emilio Jesús Gallego Arias
I'd suggest we tweet about the coq platform internships, the 8.11 release
some other news
then this
Karl Palmskog (Jan 28 2020 at 19:06):OK, as long as it's on the TODO list, I won't complain
Anton Trunov (Jan 28 2020 at 19:06):Emilio commented that way after I suggested to tweet about that post :)
Anton Trunov (Feb 02 2020 at 21:33):@Théo Zimmermann I just learned about conda.io and would like to try it in a class I’m going to teach. I installed coq8.11 and now I’m wondering how one goes about adding more stuff to the basic package. I’d like to have CoqIDE and/or VS Coq and also MathComp. Could you please point me in the right direction?
Anton Trunov (Feb 02 2020 at 21:34):(Not sure if this is the right room to discuss this topic)
Théo Zimmermann (Feb 03 2020 at 11:52):Hi @Anton Trunov, unfortunately I have very poor knowledge of this package manager. I've just tried to use it to install Coq + coq_jupyter in CoCalc because I'm starting to teach a Coq class with Jupyter today. If you are interested, I'll let you know how it goes. I'm also in contact with the Coq package maintainer in Conda, so we could further investigate your questions together if you want. When does your class start?
Anton Trunov (Feb 03 2020 at 11:54):@Théo Zimmermann Coq + coq_jupyter sounds awesome! Sure, I’d like to join to the Coq Conda project. The class starts in about two weeks.
Anton Trunov (Feb 03 2020 at 11:54):I’d love to learn more about coq_jupiter and your experience with that when you have the time.
Karl Palmskog (Feb 03 2020 at 15:37):I'm also teaching a course, but on HOL4, all material here, maybe something can be useful for Coq teaching? https://kth-step.github.io/itppv-course/
Karl Palmskog (Feb 03 2020 at 15:38):(maybe a long shot, and not the packaging for sure, SML has essentially no community-specific infrastructure for packages)
Anton Trunov (Feb 03 2020 at 15:40):@Karl Palmskog Thanks for sharing. Cool slides! Are there any lecture notes?
Karl Palmskog (Feb 03 2020 at 15:41):basically we have lecture slides + exercises
Karl Palmskog (Feb 03 2020 at 15:43):if you want slides for almost the "whole" course, rather than just the parts we have done so far, you can look at Thomas Tuerk's slides, which we are building on but heavily modifying: https://hol-theorem-prover.org/hol-course-print.pdf
Karl Palmskog (Feb 03 2020 at 15:43):his LaTeX sources: https://github.com/thtuerk/ITP-course
Anton Trunov (Feb 03 2020 at 15:44)::+1: Nice! Thanks again
Karl Palmskog (Feb 03 2020 at 15:44):right, also there's all the exercises he used: https://hol-theorem-prover.org/hol-exercises.tar.gz
Karl Palmskog (Feb 05 2020 at 14:35):@Anton Trunov I've now archived the old ALEA repo, maybe you can link to it from the new ALEA README (has a bunch of releases): https://github.com/coq-contribs/random/
Anton Trunov (Feb 05 2020 at 14:39):I opened an issue about that and CC’ed you.
Anton Trunov (Feb 05 2020 at 14:39):btw, should we close https://github.com/coq-community/manifesto/issues/55 ?
Karl Palmskog (Feb 05 2020 at 14:47):done
Anton Trunov (Feb 05 2020 at 14:47):thanks
Karl Palmskog (Feb 07 2020 at 17:25):hmm, I'm thinking about breaking off "Programming Languages" from "Verified Software" in awesome-coq, since I'm not sure how pure metatheory for a PL can count as verified software
Anton Trunov (Feb 07 2020 at 18:18)::+1:
Anton Trunov (Feb 07 2020 at 18:29):I’m wondering about project badges: should we have special badge(s) for coq-community projects that are available for some package managers like opam, Nix, etc.?
Karl Palmskog (Feb 07 2020 at 18:30):would be nice for sure
Karl Palmskog (Feb 07 2020 at 18:31):assuming they don't need a lot of maintenance...
Anton Trunov (Feb 07 2020 at 18:32):Great! I guess I’ll move this as a manifesto issue
Karl Palmskog (Feb 07 2020 at 21:22):I've now stepped down from maintaining ATBR (and also Lemma Overloading). We used ATBR for evaluating mCoq, but that research project is basically over now, and we are moving on mostly to MathComp projects (like reglang) for proof engineering research.
Karl Palmskog (Feb 07 2020 at 21:24):we have done some collective progress on doing releases, but to be honest the manual work is still pretty horrible
Karl Palmskog (Feb 07 2020 at 21:33):@Théo Zimmermann perhaps I can count you as co-maintainer of the templates repo?
Karl Palmskog (Feb 07 2020 at 21:33):sadly I'm clueless about Nix stuff
Théo Zimmermann (Feb 08 2020 at 15:16):@Karl Palmskog Yes, add me there!
Karl Palmskog (Feb 10 2020 at 20:29):so I have a version of the development mentioned here working on Coq 8.11: https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/#comment-967
Karl Palmskog (Feb 10 2020 at 20:30):I think I'll put the usual coq-community issue to make a point...
Karl Palmskog (Feb 10 2020 at 20:31):unfortunately thre license is unknown, but can probably be figured out by contacting authors
Karl Palmskog (Feb 11 2020 at 13:08):any takers for how many months this will take (before merge or close): https://github.com/sindresorhus/awesome/pull/1697
Anton Trunov (Feb 11 2020 at 16:22):Thanks for the link! A wild guess: 3 months (I have no idea what their average review time is)
Théo Zimmermann (Feb 11 2020 at 16:26):I think less than this given the age of most open PRs.
Karl Palmskog (Feb 11 2020 at 17:10):since one has to have reviewed two PRs to open a PR, and maintainers wait for external reviews, it's probabilistic I think
Karl Palmskog (Feb 11 2020 at 17:11):exponentially distributed
Karl Palmskog (Feb 13 2020 at 09:26):nice, we got fast-tracked on the awesome-repo PR, probably thanks to good adherence to the many requirements...
Karl Palmskog (Feb 13 2020 at 14:55):hmm, I was thinking one could create some kind of meta-issue for accumulating reasonably-low-effort tasks needed for Coq and coq-community
Karl Palmskog (Feb 13 2020 at 14:56):right now a lot of them live in separate GitHub repos, and many people are not aware
Karl Palmskog (Feb 13 2020 at 14:57):@Théo Zimmermann is this appropriate as a coq-community issue, even though it might be for wider Coq ecosystem?
Théo Zimmermann (Feb 13 2020 at 14:57):Sure!
Karl Palmskog (Feb 13 2020 at 14:57):we should be more liberal with help-wanted I think
Théo Zimmermann (Feb 13 2020 at 14:58):Note that we already have things like https://github.com/issues?q=is%3Aopen+is%3Aissue+archived%3Afalse+user%3Acoq-community+label%3A%22help+wanted%22 for coq-community.
Théo Zimmermann (Feb 13 2020 at 14:58):But we could extend this to something across more repos.
Théo Zimmermann (Feb 13 2020 at 14:58): Karl Palmskog (Feb 13 2020 at 14:58):ah, maybe one can just modify the query a bit
Théo Zimmermann (Feb 13 2020 at 14:58):user:coq-community + user:coq
Karl Palmskog (Feb 13 2020 at 14:58):nice
Théo Zimmermann (Feb 13 2020 at 14:59):"help wanted" might not be the right label though
Théo Zimmermann (Feb 13 2020 at 14:59):as it does not imply low-effort
Karl Palmskog (Feb 13 2020 at 14:59):right, but good-first-issue is not great either
Théo Zimmermann (Feb 13 2020 at 15:00):well at least the meaning is clearer
Théo Zimmermann (Feb 13 2020 at 15:00):and we can try to triage what's in there
Karl Palmskog (Feb 13 2020 at 15:01): Karl Palmskog (Feb 13 2020 at 15:02):I guess this can be a good compromise, although some low-hanging fruit definitely requires expertise
Théo Zimmermann (Feb 13 2020 at 15:06):With math-comp too: https://github.com/issues?utf8=%E2%9C%93&q=is%3Aopen+is%3Aissue+archived%3Afalse+user%3Acoq-community+user%3Acoq+user%3Amath-comp+label%3A%22good+first+issue%22+
Théo Zimmermann (Feb 13 2020 at 15:07): Théo Zimmermann (Feb 13 2020 at 15:07):Anyway, I'm not a big fan of this interface for showing these issues
Théo Zimmermann (Feb 13 2020 at 15:07):Maybe we should look for an external service to help with this.
Karl Palmskog (Feb 13 2020 at 15:08):right, one might want to prioritize in some way that can't be added to GitHub issue state
Karl Palmskog (Feb 13 2020 at 15:08):but as a stand-in until we find something I think it's much better than just "help-needed" listing
Théo Zimmermann (Feb 13 2020 at 15:09):yeah
Anton Trunov (Feb 13 2020 at 16:40):@Karl Palmskog Have you seen this https://github.com/awesomo4000/awesome-provable ?
Karl Palmskog (Feb 13 2020 at 16:43):I think it may have swooshed by, I don't mind it, it's one abstraction level up from us
Anton Trunov (Feb 13 2020 at 16:43):yeah, it’s not a competitor :)
Karl Palmskog (Feb 13 2020 at 16:43):the good thing about focusing on Coq is that it fit in the PL category
Anton Trunov (Feb 13 2020 at 16:44):Maybe we could mutually link?
Karl Palmskog (Feb 13 2020 at 16:44):in my mind a good way to do marketing to SE/GitHub audience is to focus on Coq-as-PL
Karl Palmskog (Feb 13 2020 at 16:45):yeah if we accumulate a few other lists we can create a section
Karl Palmskog (Feb 13 2020 at 16:45):you could open an issue
Anton Trunov (Feb 13 2020 at 16:45):cool!
Anton Trunov (Feb 13 2020 at 16:45):I’m on it :)
Karl Palmskog (Feb 13 2020 at 16:45):we can challenge the Lean people perhaps
Anton Trunov (Feb 13 2020 at 16:46)::+1:
Karl Palmskog (Feb 13 2020 at 16:46):to be clear, first step is probably an issue in awesome-coq
Karl Palmskog (Feb 13 2020 at 16:47):this is pretty interesting stuff w.r.t. hosting of projects/communities: https://sketis.net/2019/isabelle-phabricator-server-setup https://sketis.net/2020/selfhosting-of-mercurial-repositories
Karl Palmskog (Feb 13 2020 at 16:47):BitBucket dropping Mercurial sets a pretty bad precedent indeed...
Karl Palmskog (Feb 13 2020 at 16:53):So Phabricator offers a counter-model to trends of monoculture and centralized version control, especially due to Microsoft’s Github and Atlassian’s Bitbucket.
Karl Palmskog (Feb 13 2020 at 17:10):heh, from the Phabricator website:
Written in PHP so literally anyone can contribute, even if they have no idea how to program.
Théo Zimmermann (Feb 13 2020 at 18:14):We talked about having a coq-community presence in the next DeepSpec school. Any idea when this will be?
Karl Palmskog (Feb 13 2020 at 18:19):there is nothing about it in public sources, as far as I can tell. Based on previous summer schools, it will happen in mid-July
Karl Palmskog (Feb 13 2020 at 18:22):ah, Matthieu will know, he wrote:
I will be giving lectures at the DeepSpec Summer School in July 2020
Karl Palmskog (Feb 13 2020 at 18:23):maybe we can ask him who is handling it
Théo Zimmermann (Feb 13 2020 at 18:24):Do you know who we should contact to be in the loop? The other question is whether one of us can travel to the States in July. If that's one of you, I can look into whether I can unlock some budget to pay for your trip.
Théo Zimmermann (Feb 13 2020 at 18:25):Sorry I had missed half of your message
Anton Trunov (Feb 13 2020 at 20:25):Any particular format of the presense of coq-community?
Théo Zimmermann (Feb 14 2020 at 08:12):Not clear to me yet. That was Karl's suggestion, so maybe he can say more.
Théo Zimmermann (Feb 14 2020 at 08:12):Regarding the list of good first issues in the Coq ecosystem, there is also this: https://github.com/topics/coq
Karl Palmskog (Feb 14 2020 at 11:08):Well, it was a joint idea with Bas Spitters, I imagined something like the following:
Karl Palmskog (Feb 14 2020 at 11:11):and then of course the person going there would discuss with DeepSpec faculty how we can improve visibility of (their) Coq projects, the Coq ecosystem/platform and so on
Théo Zimmermann (Feb 14 2020 at 11:23):Sounds good!
Anton Trunov (Feb 14 2020 at 11:34)::+1:
Karl Palmskog (Feb 14 2020 at 11:34):if I'd do the presentation, I would call it something like: "The Coq community and ecosystem: an overview" (add in "Platform" if that is in place)
Anton Trunov (Feb 14 2020 at 11:36):LGTM!
Karl Palmskog (Feb 14 2020 at 11:36):"platform - ecosystem - community" is a nice 'tripod' to stand on
Karl Palmskog (Feb 14 2020 at 15:41):@Anton Trunov I did some quick investigation of the problems with porting CertiCrypt
Karl Palmskog (Feb 14 2020 at 15:41):using the ALEA port
Karl Palmskog (Feb 14 2020 at 15:41):there were some really strange mismatches between Set and Type
Anton Trunov (Feb 15 2020 at 15:32):@Karl Palmskog this is interesting. @volodeyka would like to start porting CertiCrypt. Should he proceed or you are too far in the process?
Karl Palmskog (Feb 16 2020 at 00:34):The problem is also that Pierre Yves Strub said he would port it
Karl Palmskog (Feb 16 2020 at 00:35):I didn't port much, just figured out one basic problem I can describe
Anton Trunov (Feb 16 2020 at 16:07):The problem is also that Pierre Yves Strub said he would port it
Yep, I asked him if there is anything we could help him with.
Karl Palmskog (Feb 17 2020 at 09:54):@Anton Trunov so compare the following: https://github.com/EasyCrypt/certicrypt/blob/master/Lib/BoolEquality.v#L458
Karl Palmskog (Feb 17 2020 at 09:54):https://github.com/EasyCrypt/certicrypt/blob/master/Semantics/Dlist.v#L164
Karl Palmskog (Feb 17 2020 at 09:55):https://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html#DecidableSet
Karl Palmskog (Feb 17 2020 at 09:56):of course one can change EQBOOL_LEIBNIZ to have t : Set, but this has to be propagated through the entire codebase...
Karl Palmskog (Feb 17 2020 at 09:58):I wonder how the heck that went through in 8.3, maybe universe consistency checking was incomplete...
Anton Trunov (Feb 17 2020 at 10:43):Could we use DecidableEq instead of DecidableEqSet ?
Karl Palmskog (Feb 17 2020 at 11:22):the problem is not exactly the signature itself, but that the following is used: https://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html#DecidableEqDepSet
Karl Palmskog (Feb 17 2020 at 11:23):if I remember correctly, one can't get UIP and so on via Type in the same way
Anton Trunov (Feb 17 2020 at 11:43):They both use
```
Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2.
Proof (eq_dep_eq__UIP U eq_dep_eq).
afaikt
Karl Palmskog (Feb 19 2020 at 15:24):@Anton Trunov so since there is no response from P-Y Strub, I can give you and Vladimir what I have right now
Karl Palmskog (Feb 19 2020 at 15:24):it turned out to be possible to fix the DepSet stuff and so on
Karl Palmskog (Feb 19 2020 at 15:27):let me know and I can make the diff available...
Karl Palmskog (Feb 19 2020 at 15:28):if nothing else there will be more of us that understand a bit more about the structure of CertiCrypt
Anton Trunov (Feb 19 2020 at 16:17):@Karl Palmskog Thank you. Vladimir is having second thoughts about CertiCrypt since there is uncertainty. I guess will just switch to something else. If we still have time by the end of the term and the things change I think we could try and port CertiCrypt.
Emilio Jesús Gallego Arias (Feb 19 2020 at 16:18):Why Certicrypt ? Isn't that superseeded by the likes of xhl ? Is there a link to the discussion with @Pierre-Yves Strub ?
Anton Trunov (Feb 19 2020 at 16:19):@Emilio Jesús Gallego Arias Here it is https://github.com/coq-community/manifesto/issues/56
Anton Trunov (Feb 19 2020 at 16:19):CertiCrypt, because of ALEA
Anton Trunov (Feb 19 2020 at 16:20):We ported ALEA to Coq 8.11 and ALEA is used in CertiCrypt so we thought we could reanimate that too to soo if ALEA is “done"
Karl Palmskog (Feb 19 2020 at 16:21):@Emilio Jesús Gallego Arias it's basically a very large Coq project (by most standards) that has been cited a lot
Karl Palmskog (Feb 19 2020 at 16:22):for proof engineering research reasons alone, it's valuable
Karl Palmskog (Feb 19 2020 at 16:24):Bas Spitters was also interested in it for crypto reasons, one might be able to transfer CertiCrypt work from ALEA to his probability library based on HoTT
Karl Palmskog (Feb 19 2020 at 16:40):@Anton Trunov one task that would be helpful to get done regardless of CertiCrypt: an initial release of ALEA
Anton Trunov (Feb 19 2020 at 17:02):Right, we could deal with the three issues marked as “1.0.0” milestone and publish it on opam. I guess incorporating more modules from https://github.com/coq-community/alea/issues/2 could be delayed until a later time
Karl Palmskog (Feb 19 2020 at 17:12)::thumbsup:
Emilio Jesús Gallego Arias (Feb 19 2020 at 17:35):Thanks for the pointer folks, tho if Pierre-Yves is planning to maintain CertiCrypt then it should not be moved to CC, right?
Anton Trunov (Feb 19 2020 at 17:35):Yep, that’s the plan
Karl Palmskog (Feb 19 2020 at 17:36):if he wants to maintain it alone, we won't stand in the way, but I guess we're hoping that he will want to put it in CC to get benefits of automation and so on
Pierre-Yves Strub (Feb 20 2020 at 10:00):No answer from me because I’m on vacation
Pierre-Yves Strub (Feb 20 2020 at 10:03):@Emilio Jesús Gallego Arias xhl is not superseeding CertiCrypt. It is a formalization of the core logic of EasyCrypt.
Pierre-Yves Strub (Feb 20 2020 at 10:05):From our perspective (the dev. of EasyCrypt), we do not want to use CertiCrypt anymore for formalization purposes. We currently use our own tool, and if we would like to go back to Coq, we would certainly not start from a port of CertiCrypt to the last version of Coq (but would certainly use the experience we gain by developping CertiCrypt)
Pierre-Yves Strub (Feb 20 2020 at 10:07):However, I agree with @Karl Palmskog about having this kind of projects compiling with the last version of Coq. It has been cited a lot, it is a big development, and it’s a pity that you have to install Coq 8.3 to play a bit with it.
Pierre-Yves Strub (Feb 20 2020 at 10:07):I do not plan to maintain CertiCrypt alone.
Pierre-Yves Strub (Feb 20 2020 at 10:07):I offered my help to port CertiCrypt to Coq 8.11.
Pierre-Yves Strub (Feb 20 2020 at 10:08):I would be happy if Vladimir can help.
Pierre-Yves Strub (Feb 20 2020 at 10:11):When done, moving CertiCrypt to CC is IMO a good solution. (The fact that CertiCrypt has not been updated for 8 years now is a good signal that we are not interested in maintaining it).
Pierre-Yves Strub (Feb 20 2020 at 10:16):I don’t know what is Vladimir internship topic, but I can only say if he wants to formalize crypto primitives, IMO, that are today better solutions :)
Pierre-Yves Strub (Feb 20 2020 at 10:16):Anyway, maybe should we have a quick chat for organizing ourselves on the CertiCrypt side.
Pierre-Yves Strub (Feb 20 2020 at 10:16):EOF (going back on vacation)
Karl Palmskog (Feb 20 2020 at 10:30)::thumbsup: (all that sounds good to me)
Bas Spitters (Feb 20 2020 at 11:25):@Karl Palmskog @Anton Trunov Interesting! I agree with @Pierre-Yves Strub that this would be mostly for legacy purposes, but the development itself is very interesting.
Bas Spitters (Feb 20 2020 at 11:26):I would imagine that most of the library would just work at the Set level.
Doing such a change should be doable, we did it a couple of times for corn. It might take a day or two though, if you are unlucky.
Bas Spitters (Feb 20 2020 at 11:36):@Anton Trunov @Karl Palmskog @Pierre-Yves Strub We are also interested in what it would take to import EC into Coq. We've been thinking about it a little, I can say more if there's an interest.
One component will be the addition of rewriting to Coq that Theo Winterhalter is working on.
Karl Palmskog (Feb 20 2020 at 12:32):OK, I think I will just put the current state of my Set/Type stuff in a fork of P-Y's repo, I resolved the problems discussed above, and it should be quite straightforward from there
Emilio Jesús Gallego Arias (Feb 20 2020 at 16:33):Hi @Pierre-Yves Strub, thanks for the comments, I wish you a nice holidays.
I'd like to remark this particular comment:
if we would like to go back to Coq, we would certainly not start from a port of CertiCrypt to the last version of Coq (but would certainly use the experience we gain by developping CertiCrypt)
IMHO that's a situation similar to the discussion we had about coq-bits, that is to say, a development which is interesting as an artifact but not suitable for further use / development.
I still wonder then if CC is the right place for such projects; I still get the impression that archival is not what I'd like to find there.
Théo Zimmermann (Feb 20 2020 at 16:36):The point is to have a community effort to maintain an interesting artifact with newer Coq versions. Having these projects within coq-community makes this task easier than if these projects are kept out. Of course, this means that the objective is slightly more broad than for instance ocaml-community.
Karl Palmskog (Feb 20 2020 at 16:38):I'd say we have quite good consensus among the CC org owners that "interesting" does not necessarily mean "recommended for use" (but regular members can/should be polled at some point)
Emilio Jesús Gallego Arias (Feb 20 2020 at 16:43):Indeed that's my main worry, dissonance with ocaml-community for example.
@Karl Palmskog owners do not worry me in this case; I'm more worried about users getting confused about the status of things. Maybe the right solution would be to add "badges" [you already have it folks?]
Emilio Jesús Gallego Arias (Feb 20 2020 at 16:44):A badge could classify CC entries in categories such as "artifact", "actively developed", "recommended / base lib", etc...
Emilio Jesús Gallego Arias (Feb 20 2020 at 16:44):I dunno, but that would retain the organizational unity while providing at the same time a quick overview of the status
Emilio Jesús Gallego Arias (Feb 20 2020 at 16:45):For example something can be maintained but still have the category of "artifact" [artifacts for me are intrinsically associated to papers, and usually not meant for wide consumption]
Théo Zimmermann (Feb 20 2020 at 16:49):Absolutely, I'm very supportive of this badge idea. In the meantime, some repositories use GitHub tags for some of this purpose.
Théo Zimmermann (Feb 20 2020 at 16:51):Indeed that's my main worry, dissonance with ocaml-community for example.
I'm not in control of the path that ocaml-community has decided to take. It is a valid one as well. But ocaml-community was created after coq-community was announced with clear objectives. They chose to inspire from part of them, and to deviate of some.
Karl Palmskog (Feb 20 2020 at 16:58):I also think we can harmonize tags and badges, unfortunately paper-artifact can be ambiguous to outsiders
Karl Palmskog (Feb 20 2020 at 16:58):something like research-artifact may be better
Théo Zimmermann (Feb 20 2020 at 16:59)::+1:
Théo Zimmermann (Feb 20 2020 at 16:59):Or even research-prototype if we want to insist on the non user-ready status.
Karl Palmskog (Feb 20 2020 at 17:00):I think it's clear that coq-community will be much more research-oriented than ocaml-community for the foreseeable future, not least due to individual member goals
Karl Palmskog (Feb 20 2020 at 17:02):I don't mind advertising this more clearly
Théo Zimmermann (Feb 20 2020 at 17:04):Next week, I'll look into buying a domain name for coq-community and starting a website. This should help clarify some of the goals and that not all projects are on the same footing.
Karl Palmskog (Feb 20 2020 at 17:06)::thumbsup: - will have the :tada: ready
Karl Palmskog (Feb 20 2020 at 17:07):@Théo Zimmermann btw, I was looking to promote awesome-coq by pinning it on GitHub, but this means another repo has to be unpinned...
Théo Zimmermann (Feb 20 2020 at 17:07):Sure, that's life.
Karl Palmskog (Feb 20 2020 at 17:07):I'm leaning towards docker-coq
Karl Palmskog (Feb 20 2020 at 17:08):very important, but very specialized
Théo Zimmermann (Feb 20 2020 at 17:08):What about Corn? More diversity.
Karl Palmskog (Feb 20 2020 at 17:09):OK sounds good
Karl Palmskog (Feb 20 2020 at 19:04):@Anton Trunov here's my experiment with CertiCrypt, it's one "giant" commit that solves the DepSet problems but admits some proofs along the way: https://github.com/palmskog/certicrypt/tree/depset-8.11
Anton Trunov (Feb 20 2020 at 19:28):Thanks for sharing, Karl. I had to put that on a slow burner, though, sorry. That’s because of the time limits we have for this internship project.
Karl Palmskog (Feb 20 2020 at 19:31):fine by me, I'll just comment in the issue and maybe someone else can take note
Anton Trunov (Feb 20 2020 at 19:31)::+1:
Karl Palmskog (Feb 20 2020 at 20:19):looks like Kevin added some Coq-positive stuff in his latest blogpost (https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/)
[Note added 14th Feb: thanks to Théo Zimmermann for pointing out to me on Twitter that Coq has a Discourse forum. Young people wanting to learn Coq — try asking some beginner questions there. Ask how to make class groups of number fields! Let’s get more serious mathematics done in Coq! It’s an extremely powerful system! ]
Karl Palmskog (Feb 20 2020 at 20:20):this is something I've been working towards:
Sarah Loos from Google AI explicitly raised this issue [of multiple proofs of theorem] with me at AITP last year. She was bemoaning the fact that in a typical database, a theorem will have exactly one proof. Everyone knows that different proofs can add different value to a situation, by giving different insights. She wants more proofs! These people need our input!
Karl Palmskog (Feb 24 2020 at 20:27):@Anton Trunov one issue here is that the "description" field can't be assumed to be rendered in Markdown: https://github.com/coq-community/alea/blob/master/meta.yml#L16
Karl Palmskog (Feb 24 2020 at 20:27):for example, it is used in the OPAM file (and thus by opam show), and potentially in dune and so on
Karl Palmskog (Feb 24 2020 at 20:28):if there needs to be URLs there, I recommend having them in full
Anton Trunov (Feb 25 2020 at 12:24):@Karl Palmskog thanks, I missed that during review
Karl Palmskog (Feb 25 2020 at 15:36):@Anton Trunov also wondering about ALEA license, the new repo says plain GPL2 while original repo was LGPL
Karl Palmskog (Feb 25 2020 at 15:39):in fact there is no GPL-2.1 as mentioned in current meta.yml, and license file seems to be missing
Anton Trunov (Feb 25 2020 at 15:39):yep, I just discovered the same thing :)
Karl Palmskog (Feb 25 2020 at 15:40):(2.0 and 3.0 are the only relevant versions of plain GPL)
Anton Trunov (Feb 25 2020 at 15:40):@Karl Palmskog do you have the link where it says the license is LGPL?
Karl Palmskog (Feb 25 2020 at 15:44):LICENSE file in coq-contribs repo
Anton Trunov (Feb 25 2020 at 15:47):Thanks. Should it be LGPL-2.1-only or LGPL-2.1-or-later?
Karl Palmskog (Feb 25 2020 at 15:48):I tried to have Pierre Cortieau clarify, but we did not clear that up, so we have to assume that it's 'only'
Anton Trunov (Feb 25 2020 at 15:49):got it, thanks again
Gregory Malecha (Mar 04 2020 at 21:40):does anyone know where coq's implementation of discrimintion trees is and how deep they go?
Karl Palmskog (Mar 11 2020 at 19:18):@Théo Zimmermann sorry to pile on, but is the domain thing still on your agenda?
Théo Zimmermann (Mar 11 2020 at 19:20):@Karl Palmskog Yes, I've asked my team assistant about it and it seems the easiest path is for me to buy the domain name in my own name and have Inria reimburse me, so I can take care of this tomorrow.
Karl Palmskog (Mar 11 2020 at 19:24):great, let me know if I can help, e.g., we could have some simple static stand-in page in the repo coq-community.github.io (which would appear at the domain) until we set up something more dynamic
Théo Zimmermann (Mar 11 2020 at 19:27):Yes, if you can create this repo, that would be great.
Karl Palmskog (Mar 11 2020 at 19:31):OK sure. As you might know, the main complication you will have to deal with is to point DNS for the domain to GitHub's servers (https://help.github.com/en/github/working-with-github-pages/managing-a-custom-domain-for-your-github-pages-site) - see the part about DNS A records
Karl Palmskog (Mar 11 2020 at 19:32):# GitHub DNS server IPs for "A" record
185.199.108.153
185.199.109.153
185.199.110.153
185.199.111.153
Yes, I'm always doing this for my own website.
Maxime Dénès (Mar 12 2020 at 08:26):Yes, I've asked my team assistant about it and it seems the easiest path is for me to buy the domain name in my own name and have Inria reimburse me, so I can take care of this tomorrow.
@Théo Zimmermann I got the opposite information from my managers
Maxime Dénès (Mar 12 2020 at 08:27):and I'd bet they are more aware than team assistants for this matter
Maxime Dénès (Mar 12 2020 at 08:27):We can talk a bit this afternoon about it if you like.
Théo Zimmermann (Mar 12 2020 at 13:27):OK @Maxime Dénès, I didn't know you had got an answer. Are you available to talk about this now or soonish?
Maxime Dénès (Mar 12 2020 at 14:21):now is fine
Karl Palmskog (Mar 12 2020 at 15:43):@Théo Zimmermann was there any conclusion on the domain issue?
Théo Zimmermann (Mar 12 2020 at 16:26):There is a person at Inria that is in charge of this. I'm going to contact her. This might delay the domain name creation for some time, but it's better to do things properly.
Karl Palmskog (Mar 12 2020 at 16:32):OK
Théo Zimmermann (Mar 13 2020 at 11:15):@Karl Palmskog I've launched the process for creating the domain name. Let's see how long it will take. In any case, it would be good to have a minimal page available at coq-community.github.io ASAP, since I've already provided this link.
Karl Palmskog (Mar 13 2020 at 11:38):@Théo Zimmermann OK, I will put something there later this afternoon
Gregory Malecha (Mar 13 2020 at 20:53):is there a way to determine whether a goal is a Class? I would like to say something like tryif is_class G (* G is the goal *) then solve [ typeclasses eauto with typeclass_instances ] else idtac
Karl Palmskog (Mar 13 2020 at 20:56):@Gregory Malecha this is probably not the best channel for these kinds of question, I don't think, e.g., Matthieu is monitoring
Gregory Malecha (Mar 13 2020 at 20:56):is it best to ask on /coq
Karl Palmskog (Mar 13 2020 at 20:56):yes, either there or in the Discourse forum
Gregory Malecha (Mar 13 2020 at 20:56):ok, thanks
Karl Palmskog (Mar 13 2020 at 20:57):if you think the answer is of general value, I recommend the Discourse
Karl Palmskog (Mar 13 2020 at 20:57):much more searchable etc.
Gregory Malecha (Mar 13 2020 at 20:57):thanks
Karl Palmskog (Mar 13 2020 at 22:25):https://coq-community.github.io - basic static website - first big enhancement would probably be to generate list of projects via GitHub queries
Bas Spitters (Mar 14 2020 at 09:06):@Karl Palmskog You may want to change the order to not make this look like a list of abandoned projects:
"the initial author has stopped maintaining the project and someone else is volunteering to do so;"
Bas Spitters (Mar 14 2020 at 09:08):Maybe also mention something about the upsides: good opam integration, CI,machine learning, ... and the relation to coq-contribs.
Nice work in any case !
Bas Spitters (Mar 14 2020 at 09:09):Is there any order in the "current projects" ?
Karl Palmskog (Mar 14 2020 at 12:43):@Bas Spitters this was a very quick hack-job, I just copy-pasted projects from the browser, so order is as "last modified" as of Mar 13
Karl Palmskog (Mar 14 2020 at 12:44):I can change the initial stuff on hosting and add something about applications you mentioned
Karl Palmskog (Mar 14 2020 at 17:35):another thing to consider may be if we should have some kind of top-level project categories that include non-verification projects, e.g., Documentation, Interface, Meta, Automation
Karl Palmskog (Mar 14 2020 at 17:36):that should make a project list a lot easier to navigate
Karl Palmskog (Mar 15 2020 at 21:09):@Bas Spitters what do you think of the following approach to categorizing/listing projects? https://coq-community.github.io/index.html
Bas Spitters (Mar 15 2020 at 21:15):@Karl Palmskog Seems reasonable enough. Thanks!
Karl Palmskog (Mar 15 2020 at 21:18):ideally we would store categorization metadata in each project and extract it dynamically
Karl Palmskog (Mar 15 2020 at 21:19):for OPAM, we have categories already, but it seems actually many projects are not pure Coq projects anymore
Karl Palmskog (Mar 15 2020 at 21:19):so maybe it's warranted to make a distinction between "general category" and "opam category" in metadata
Karl Palmskog (Mar 17 2020 at 08:34):@Théo Zimmermann so what do you think of the categorization? https://coq-community.github.io
Karl Palmskog (Mar 17 2020 at 08:40):can we maybe get a retweet on this one from the Twitter CoqLang gods (others also welcome to retweet): https://twitter.com/TaliaRinger/status/1239784878993887232
Stuck in your house and need something to read? Want to feel productive while working from home? How about reading our 120 page survey paper on proof engineering, now on arXiv: https://arxiv.org/abs/2003.06458
- Talia Ringer (@TaliaRinger) Théo Zimmermann (Mar 17 2020 at 14:50):@Karl Palmskog OK, now in the queue.
Théo Zimmermann (Mar 17 2020 at 14:50):How is index.html generated? Is it from index.md? I spotted typos to fix but wouldn't want to mess things up.
Karl Palmskog (Mar 17 2020 at 14:51):yes, just generated via pandoc: pandoc -s -o index.html index.md, feel free to update
Théo Zimmermann (Mar 17 2020 at 14:51):OK
Karl Palmskog (Mar 17 2020 at 14:52):I'm not sure that's how we want to do it further on, but it was the fastest I could think of to get the static page
Théo Zimmermann (Mar 17 2020 at 14:53)::+1:
Théo Zimmermann (Mar 17 2020 at 14:54):Unfortunately, regenerating the HTML using the same command changes a bunch of unrelated stuff :S
Karl Palmskog (Mar 17 2020 at 14:54):we may have different versions of pandoc
Karl Palmskog (Mar 17 2020 at 14:55):but doesn't matter if the content is the same
Théo Zimmermann (Mar 17 2020 at 15:02):I think the introduction should additionally mention that being part of coq-community makes transition from one maintainer to the next easier.
Théo Zimmermann (Mar 17 2020 at 15:02):And possibly link to the contributing guide.
Théo Zimmermann (Mar 17 2020 at 15:03):But very good job, thanks!
Théo Zimmermann (Mar 17 2020 at 15:07):Coqoban does probably better fit the Documentation and Tutorials category.
Karl Palmskog (Mar 17 2020 at 15:07):in some sense, but also, it's a "verified puzzle"
Théo Zimmermann (Mar 17 2020 at 15:08):And even if we don't have any editorial committee, we should start putting some badges on projects to highlight recommended projects and possibly alert on projects of lower quality.
Théo Zimmermann (Mar 17 2020 at 15:08):For instance with a :star: and a :warning:
Karl Palmskog (Mar 17 2020 at 15:08):I would say "experimental" rather than "low quality"
Théo Zimmermann (Mar 17 2020 at 15:08):Sure
Théo Zimmermann (Mar 17 2020 at 15:08):or WIP
Théo Zimmermann (Mar 17 2020 at 15:09):what I mean is that we should write explicitly that not all projects hosted in coq-community are meant to be top quality.
Théo Zimmermann (Mar 17 2020 at 15:09):As we have already seen, some people might misunderstand coq-community hosting as a label of quality.
Karl Palmskog (Mar 17 2020 at 15:09):yeah good point
Karl Palmskog (Mar 17 2020 at 15:10):but how do you think we should store categories and labels? meta.yml?
Théo Zimmermann (Mar 17 2020 at 15:20):possibly yes
Théo Zimmermann (Mar 17 2020 at 15:21):FYI coq-community.github.io now redirects to coq-community.org but coq-community.org DNS records are not yet configured to point to coq-community.github.io. Thus, the website will be unavailable until this is done (hopefully it won't take more than a day or two).
Karl Palmskog (Mar 17 2020 at 15:21):sounds good
Karl Palmskog (Mar 17 2020 at 15:22):I'll keep the :tada:s ready
Karl Palmskog (Mar 17 2020 at 15:23):oh right, another meta-issue that may not even deserve its own GitHub issue: given that synopses and descriptions are used in so many contexts for different purposes, we may want to ensure that "Coq" always occurs once in all of them
Karl Palmskog (Mar 17 2020 at 15:24):and maybe our README.md template should include a link to the Coq website somewhere
Théo Zimmermann (Mar 17 2020 at 15:24):interesting thought indeed!
Karl Palmskog (Mar 17 2020 at 15:24):all for marketing reasons and so on
Karl Palmskog (Mar 17 2020 at 15:26):case in point: "This library develops some basic set theory" -> "This library develops some basic set theory in Coq"
Théo Zimmermann (Mar 17 2020 at 20:25):@Karl Palmskog I have a motivated intern starting end of May to maintain and improve the bot. There will be many things to do and he won't be operational immediately, but it will be a good time to submit feature requests for automation, in particular for coq-community.
Karl Palmskog (Mar 18 2020 at 15:58):@Théo Zimmermann are you sure the DNS will be updated? 24+ hours is on the long side
Théo Zimmermann (Mar 18 2020 at 16:00):I know that my request has been transmitted to the relevant people, but I don't know when they will take the requested action. Due to many people working from home because of COVID-19, there might be additional delays. Unfortunately, GitHub requires that the CNAME record be configured before the DNS are, and I don't have a way to coordinate with the people setting the DNS.
Karl Palmskog (Mar 18 2020 at 16:01):I see, I guess we'll just wait and see then
Karl Palmskog (Mar 20 2020 at 12:13):http://coq-community.org is up! :tada:
Karl Palmskog (Mar 20 2020 at 12:14):however, we don't have a certificate for https yet (should appear within 24h, then I'll switch to https only)
Karl Palmskog (Mar 20 2020 at 12:28):now it works, that was fast: https://coq-community.org/
Théo Zimmermann (Mar 20 2020 at 12:59):Great! I think we should at least insert the :star: and the :warning: before we advertise this website too much.
Karl Palmskog (Mar 20 2020 at 13:01):well, not only the website works, but also project websites like: https://coq-community.org/reglang
Guillaume Claret (Gitter import) (Mar 20 2020 at 13:01)::tada:
Théo Zimmermann (Mar 20 2020 at 13:02)::rocket:
Karl Palmskog (Mar 20 2020 at 13:02):@Théo Zimmermann can we use those star and warning emojis exactly, or do you have a preference for some specific ones?
Théo Zimmermann (Mar 20 2020 at 13:02):those look good to me
Karl Palmskog (Mar 20 2020 at 13:04):OK, so star in my book would be at least: AAC Tactics, Math Classes, VSCoq, docker-coq
Karl Palmskog (Mar 20 2020 at 13:05):warnings based on READMEs: ParamCoq, Exact real arithmetic, bits
Paolo Giarrusso (Mar 20 2020 at 13:09):What’s the semantics of star? As a vscoq fan and used, I wouldn’t call it mature, especially next to math-classes.
Paolo Giarrusso (Mar 20 2020 at 13:09):(Not sure @Maxime Dénès would disagree)
Théo Zimmermann (Mar 20 2020 at 13:10):That's a good question. We have given it much advertising so far but maybe too much?
Karl Palmskog (Mar 20 2020 at 13:10):well, it was based on that people reported it usable
Karl Palmskog (Mar 20 2020 at 13:10):and VSCode support is a hot topic, etc.
Théo Zimmermann (Mar 20 2020 at 13:12):Paramcoq is already probably more of a :star: than a :warning: (I think, but I'm not a user myself). When people put "this is experimental" in their doc, they tend to never remove it.
Karl Palmskog (Mar 20 2020 at 13:13):that's probably true, yes
Paolo Giarrusso (Mar 20 2020 at 13:20):I have recommended vscoq to colleagues, but the experience includes Coq crashing, interruption failing, etc.
Paolo Giarrusso (Mar 20 2020 at 13:21):But if you come in expecting a finished product, you’ll be very disappointed, I think.
Théo Zimmermann (Mar 20 2020 at 13:21):So indeed, that sounds to early to give it a :star:
Théo Zimmermann (Mar 20 2020 at 13:22):Not having a :star: won't prevent people to use it BTW
Paolo Giarrusso (Mar 20 2020 at 13:22):(Sorry, “coq crashing “ isn’t accurate, but you must restart the plugin often enough)
Emilio Jesús Gallego Arias (Mar 21 2020 at 00:40):https://uwaterloo.ca/news/news/personality-plays-key-role-whether-developers-can-contribute-0
Emilio Jesús Gallego Arias (Mar 21 2020 at 00:41):Interesting study with loads of Github data "Personality plays key role in whether developers can contribute to open source projects"
Karl Palmskog (Mar 21 2020 at 12:48):@Théo Zimmermann do you think it would be worthwhile at some point to use GitHub "projects" to track (say, automation) tasks for coq-community? in the near future or only after your intern starts?
Théo Zimmermann (Mar 21 2020 at 13:18):You can just open issues in the bot bug tracker.
Théo Zimmermann (Mar 21 2020 at 13:20):A project can still be useful to gather all relevant issues about the topic but all the automation that would work without the bot would be outside of the scope of my intern's tasks.
Karl Palmskog (Mar 21 2020 at 16:56):so nothing related to the OPAM index/archive unless it can be done with the bot?
Karl Palmskog (Mar 21 2020 at 16:58):I would argue there is some low-hanging fruit there
Théo Zimmermann (Mar 22 2020 at 08:22):Well, feel free to raise issues in the relevant repositories to propose automation. We (you and I and possibly others) might work on them together. But I won't put my intern on non-bot automation issues as he's really looking for a consistent programming project (the bot) rather than a myriad of small infrastructure tasks.
Cyril Cohen (Apr 15 2020 at 14:10):Hi, I am in the process of exporting gitter channels (public) data to zulip, (it can be done only once, during the creation of the zulip chatroom), do you wish that I export the data of this channel too?
Anton Trunov (Apr 15 2020 at 14:11):Hi @Cyril Cohen! I think that would certainly be useful. @Théo Zimmermann @Karl Palmskog what do you think?
Théo Zimmermann (Apr 15 2020 at 14:12):Yes, I agree.
Karl Palmskog (Apr 15 2020 at 16:57):I'm not a huge fan of losing public general access to chat content, but I bow to the majority here
Théo Zimmermann (Apr 15 2020 at 16:58):I seriously hope that until Zulip adds anonymous access, we will set up the public archive mechanism they provide.
Karl Palmskog (Apr 15 2020 at 17:34):but does the public archive actually work right now? if so, I would have expected Lean to use it
Cyril Cohen (Apr 15 2020 at 18:17):https://leanprover-community.github.io/archive/
Karl Palmskog (Apr 15 2020 at 18:32):@Cyril Cohen to my knowledge, that's an ad-hoc solution they rolled themselves, that doesn't provide search (at least not inline)
Karl Palmskog (Apr 15 2020 at 18:40):as seen here, it doesn't always update automatically: https://github.com/leanprover-community/leanprover-community.github.io/commits/master
Théo Zimmermann (Apr 15 2020 at 18:51):I don't know if they use the official tool or something else but Zulip does provide a tool: https://zulipchat.com/for/open-source/#public-archive
Cyril Cohen (Apr 15 2020 at 18:52):@Théo Zimmermann It is pointing to Rob's tool that was originally developed for lean as @Karl Palmskog mentionned
Cyril Cohen (Apr 15 2020 at 18:53):One good sign is that Zulip main contributor is personally invested in a core feature https://github.com/zulip/zulip/pull/12728
Théo Zimmermann (Apr 15 2020 at 18:53):Interesting!
Dan Frumin (Gitter import) (Apr 16 2020 at 09:27):So this chat will be moving to Zulip?
Théo Zimmermann (Apr 16 2020 at 09:28):Yes, or at least we will experiment with it. (We can always come back if it doesn't work out.)
Bas Spitters (Apr 16 2020 at 10:49):@Cyril Cohen @Karl Palmskog There is a free plan. Apparently, that's what they got at the category zullip. We still need to contact them about the hott zulip.
https://hott.zulipchat.com/#narrow/stream/228519-general/topic/Hosting.20and.20history
Théo Zimmermann (Apr 16 2020 at 10:57):@Bas Spitters We are aware of this and I think that if Cyril is moving forward, it means that he has got a positive answer from them.
Gregory Malecha (May 03 2020 at 20:39):does anyone know how to record dependency information in the meta.yml file from coq-templates?
Karl Palmskog (May 03 2020 at 21:02):@Gregory Malecha sure, what you want to know?
Gregory Malecha (May 03 2020 at 21:02):how do i record dependency information. it seems like the two examples, chapar and aac_tactics don't have dependencies
Gregory Malecha (May 03 2020 at 21:03):e.g. my project depends on coq-ext-lib and coq-template-coq
Karl Palmskog (May 03 2020 at 21:03):here's another example:
dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{(>= "1.9" & < "1.11~") | (= "dev")}'
nix: ssreflect
description: |-
[MathComp](https://math-comp.github.io) 1.9.0 or later (`ssreflect` suffices)
also iris and stdpp
Karl Palmskog (May 03 2020 at 21:04):basically, it's a list, so each dependency has to start with -
Karl Palmskog (May 03 2020 at 21:04):@Gregory Malecha so which versions of coq-ext-lib and coq-template-coq?
Gregory Malecha (May 03 2020 at 21:04):i see
Gregory Malecha (May 03 2020 at 21:04):ok, great
Karl Palmskog (May 03 2020 at 21:05):I can vet the meta.yml for you if you write something
Gregory Malecha (May 03 2020 at 21:05):that would be great
Gregory Malecha (May 03 2020 at 21:06):another issue that i have (which is probably not a solved issue) is that my code depends on clang
Gregory Malecha (May 03 2020 at 21:06):which is obviously not an ocaml dependency
Karl Palmskog (May 03 2020 at 21:06):that can be added as an OPAM dependency
Gregory Malecha (May 03 2020 at 21:06):how?
Karl Palmskog (May 03 2020 at 21:07):usually "conf-clang" {build}
Karl Palmskog (May 03 2020 at 21:07):if it's only in the build phase
Karl Palmskog (May 03 2020 at 21:07):there is an OPAM package called conf-clang that specifies for each OS how one should check that clang is installed
Gregory Malecha (May 03 2020 at 21:07):ah
Gregory Malecha (May 03 2020 at 21:07):ok
Gregory Malecha (May 03 2020 at 21:08):the project contains two pieces, a coq formalization and a tool built on clang
Gregory Malecha (May 03 2020 at 21:08):so clang is needed in "all" phases
Karl Palmskog (May 03 2020 at 21:08):well, you can just omit {build}
Gregory Malecha (May 03 2020 at 21:08):ok
Gregory Malecha (May 03 2020 at 21:09):that is great
Karl Palmskog (May 03 2020 at 21:09):note that there is also conf-g++
Karl Palmskog (May 03 2020 at 21:09):so for some projects we write ("conf-g++" {build} | "conf-clang" {build}) when they are agnostic to compiler
Gregory Malecha (May 03 2020 at 21:10):i see
Gregory Malecha (May 03 2020 at 21:10):thanks
Karl Palmskog (May 03 2020 at 21:11):what you might want to do is to have separate package definitions for the tool and Coq formalization
Karl Palmskog (May 03 2020 at 21:12):it's all contextual, but it's sometimes nice to provide pure Coq code for others to depend on
Gregory Malecha (May 03 2020 at 21:12):so they just clone out of the same repo but have different build targets?
Karl Palmskog (May 03 2020 at 21:12):right
Gregory Malecha (May 03 2020 at 21:12):is there a standard naming convention for that
Karl Palmskog (May 03 2020 at 21:12):not really
Gregory Malecha (May 03 2020 at 21:12):the whole project is called cpp2v
Gregory Malecha (May 03 2020 at 21:13):coq-cpp2v and coq-cpp2v-bin
Karl Palmskog (May 03 2020 at 21:13):I can show you how we did it in CoqHammer
Gregory Malecha (May 03 2020 at 21:13):or something liekthat
Gregory Malecha (May 03 2020 at 21:13):that would be great
Karl Palmskog (May 03 2020 at 21:13):the CoqHammer plugin (coq-hammer):
build: [make "-j%{jobs}%" {ocaml:version >= "4.06.1"} "plugin"]
install: [
[make "install-plugin"]
[make "test-plugin"] {with-test}
]
depends: [
"ocaml"
"coq" {>= "8.11" & < "8.12~"}
("conf-g++" {build} | "conf-clang" {build})
"coq-hammer-tactics" {= version}
]
the CoqHammer tactics (coq-hammer-tactics:
build: [make "-j%{jobs}%" {ocaml:version >= "4.06.1"} "tactics"]
install: [
[make "install-tactics"]
[make "test-tactics"] {with-test}
]
depends: [
"ocaml"
"coq" {>= "8.11" & < "8.12~"}
]
i see
Gregory Malecha (May 03 2020 at 21:15):great
Karl Palmskog (May 03 2020 at 21:15):ah, I assume this is related to a certain recent submission?
Gregory Malecha (May 03 2020 at 21:15):yes
Gregory Malecha (May 03 2020 at 21:16)::-)
Karl Palmskog (May 03 2020 at 21:21):the only thing that's a bit awkward right now is to modify CI configuration a bit to use both projects locally (they both have to be opam pinned from the filesystem)
Karl Palmskog (May 03 2020 at 21:21):that is, if one has two local OPAM package definitions
Karl Palmskog (May 03 2020 at 21:22):I don't think this can be supported in a general way in the Travis template, say, without a lot of awkwardness
Karl Palmskog (May 03 2020 at 21:24):specifically, the template assumes there is a single local OPAM package definition that is first pinned, then installed
Gregory Malecha (May 03 2020 at 21:27):i was assuming that i wouldn't be able to use the travis template because of my clang requirement
Karl Palmskog (May 03 2020 at 21:28):no, it can be done
Karl Palmskog (May 03 2020 at 21:29):you can see here how one adds native libraries: https://github.com/certichain/toychain/blob/master/.travis.yml#L15
Karl Palmskog (May 03 2020 at 21:30):I'd like to parameterize the Travis template with this at some point, but I don't have a lot good use cases of my own, so low on priorities list
Karl Palmskog (May 03 2020 at 21:31):basically, I'd recommend you to generate the Travis file from template, then just modify a few lines
Karl Palmskog (May 03 2020 at 21:32):this is what I did to handle the two local packages: https://github.com/lukaszcz/coqhammer/blob/coq8.11/.travis.yml#L15-L16
Gregory Malecha (May 03 2020 at 21:43):one more question. i depend on iris and stdpp but they don't release to main opam for the releases that i need
Gregory Malecha (May 03 2020 at 21:44):can you tell me how to depend on something in here (https://gitlab.mpi-sws.org/iris/opam/-/tree/master/packages/coq-stdpp) for example
Karl Palmskog (May 03 2020 at 21:49):opam doesn't really allow you to say in which repository a package is defined
Karl Palmskog (May 03 2020 at 21:49):if you want CI and installation to work, you have to add all the necessary opam repo add ... by hand
Gregory Malecha (May 03 2020 at 21:50):so i just list the dependency as usual and then document the opam repo add command?
Gregory Malecha (May 03 2020 at 21:50):that makes sense
Karl Palmskog (May 03 2020 at 21:50):right
Gregory Malecha (May 03 2020 at 21:50):thanks for your help
Karl Palmskog (May 03 2020 at 21:50):np
Karl Palmskog (May 03 2020 at 21:52):I thought coq-stdpp had dev packages? But I guess one can also use a definition directly from a Git repo
Gregory Malecha (May 03 2020 at 21:53):i'm not familiar with how dev packages work
Karl Palmskog (May 03 2020 at 21:54):we have a repository of (mostly) packages whose sources live in Git: opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
Karl Palmskog (May 03 2020 at 21:55):I think coq-stdpp lives in there with version dev. But see here for a discussion of pros and cons of using this repo and pinning directly to an OPAM package from a Git repo: https://github.com/uwplse/StructTact/issues/55
Gregory Malecha (May 03 2020 at 21:56):i see
Gregory Malecha (May 03 2020 at 21:56):thanks
Gregory Malecha (May 04 2020 at 21:00):i'm having an issue in generating README.md, in the dependencies section it seems to be copying the description once for each dependency
Karl Palmskog (May 04 2020 at 21:09):@Gregory Malecha can you give an example? Normally, one wants to have one unique description for each dependency. You can also leave out the description and see what happens
Gregory Malecha (May 05 2020 at 19:19):it is actualy copying my projects "description" over and over again
Théo Zimmermann (May 05 2020 at 20:05):it would be easier to understand with a link to some code
Gregory Malecha (May 05 2020 at 20:14):https://gist.github.com/gmalecha/4eb22d2267c502ff8bfd0fb4d4eef13f
Gregory Malecha (May 05 2020 at 20:15):when i run that through mustache
Gregory Malecha (May 05 2020 at 20:15):i get
Gregory Malecha (May 05 2020 at 20:15):This project provides an axiomatic semantics for C++ programs built on
top of the Iris framework for separation logic.
The AST is based on the AST of Clang and the project contains a standalone
tool and Clang plugin that convert C++ files into their AST.
## Meta
- Author(s):
- Gregory Malecha (initial)
- Gordon Stewart
- Abhishek Anand
- John Grosen
- License: [GNU Affero General Public License](LICENSE)
- Compatible Coq versions: master (use the corresponding branch or release for other Coq versions)
- Compatible OCaml versions: 4.05.0 or later
- Additional dependencies:
- This project provides an axiomatic semantics for C++ programs built on
top of the Iris framework for separation logic.
The AST is based on the AST of Clang and the project contains a standalone
tool and Clang plugin that convert C++ files into their AST.
- This project provides an axiomatic semantics for C++ programs built on
top of the Iris framework for separation logic.
The AST is based on the AST of Clang and the project contains a standalone
tool and Clang plugin that convert C++ files into their AST.
- This project provides an axiomatic semantics for C++ programs built on
top of the Iris framework for separation logic.
The AST is based on the AST of Clang and the project contains a standalone
tool and Clang plugin that convert C++ files into their AST.
- Coq namespace: `bedrock`
- Related publication(s): none
OK thanks. Indeed, it looks like the way the template is implemented it will look for description for each dependency, and if it is not defined in the dependency itself, it will take the global one.
Gregory Malecha (May 05 2020 at 20:19):ah, thanks
Théo Zimmermann (May 05 2020 at 20:19):We could avoid this by renaming the description within the dependency field into something else.
Théo Zimmermann (May 05 2020 at 20:19):Let me try something
Théo Zimmermann (May 05 2020 at 20:29):See https://github.com/coq-community/templates/pull/27
Last updated: Jun 03 2023 at 17:29 UTC