Stream: coq-community devs & users

Topic: imported from gitter room coq-community/Lobby


view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2018 at 18:21):

Salut tout le monde, paramcoq has been added to Coq's CI :)

view this post on Zulip 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!

view this post on Zulip Emilio Jesús Gallego Arias (Nov 13 2018 at 18:45):

Salut @Théo Zimmermann , merci !

view this post on Zulip Emilio Jesús Gallego Arias (Nov 13 2018 at 18:45):

:D

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Nov 13 2018 at 19:04):

Indeed, it could be. Feel free to tell people to come here.

view this post on Zulip Karl Palmskog (Nov 15 2018 at 01:44):

will coqpp be mandatory for plugins in 8.10, or will ml4 still work?

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 04:41):

Hi @Karl Palmskog , ml4 will likely not supported in 8.10

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 05:15):

Here is a proof of concept https://github.com/ejgallego/coq-cplugin

view this post on Zulip Karl Palmskog (Nov 15 2018 at 14:49):

@Emilio Jesús Gallego Arias thanks, that's just what I've been looking for

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 15:04):

No prob

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 15:06):

@Karl Palmskog not yet

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 15:06):

I recommend developing the ML parts with Dune tho

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Nov 15 2018 at 15:08):

OK sounds good

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 15:08):

in general

view this post on Zulip Karl Palmskog (Nov 15 2018 at 15:09):

we tend to only target the released Coq versions though

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 15:09):

you can do that too, but you won't a composed build

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 15:10):

YMMV

view this post on Zulip Karl Palmskog (Nov 15 2018 at 15:11):

so the plan is to throw out coq_makefile eventually?

view this post on Zulip Karl Palmskog (Nov 15 2018 at 15:11):

and everybody does coq_dune?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 15:12):

instead of having to mess with flags

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 15:16):

indeed

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 15:16):

that's _so_ convenient

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 15:16):

when composing a new global set of rules is created

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 15:17):

it also uses OCaml -opaque which means a big practical speedup, etc...

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Nov 15 2018 at 15:20):

for example, we often only want to build the OCaml project without checking all the proofs

view this post on Zulip Karl Palmskog (Nov 15 2018 at 15:20):

or do just-enough-proof-checking-to-get-extracted-file

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Nov 15 2018 at 15:35):

distributed systems verification projects have this absurd ratio of proofs-to-code

view this post on Zulip Karl Palmskog (Nov 15 2018 at 15:35):

maybe 20:1 or more in my experience

view this post on Zulip Karl Palmskog (Nov 15 2018 at 15:36):

code gets extracted in 20 seconds, proofs take 1h to check

view this post on Zulip Karl Palmskog (Nov 15 2018 at 15:36):

at least they're not tightly coupled

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 15:43):

you are talking about verdi?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 15:43):

and verdi-raft?

view this post on Zulip Karl Palmskog (Nov 15 2018 at 15:43):

for example, we're working on new projects

view this post on Zulip 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

view this post on Zulip 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 :)

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 15:45):

we were discussing some tricks used in math-comp in fact :)

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 15:46):

I also wanted to write you about incremental compilation

view this post on Zulip 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 :/

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Nov 15 2018 at 15:55):

I think in big projects Proof using. is feasible, we were able to automate annotations

view this post on Zulip Karl Palmskog (Nov 15 2018 at 15:56):

basically, one can run auto-annotate once a week or something

view this post on Zulip Karl Palmskog (Nov 15 2018 at 15:57):

anyway, even selection/parallelism at the file level can help a lot

view this post on Zulip Karl Palmskog (Nov 15 2018 at 15:57):

and then tricks like using a 32-bit Coq (we get 20% speedup or so)

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 15:58):

flambda can get you another 10% easily

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 15:58):

with the right options, as documented on INSTALL

view this post on Zulip Karl Palmskog (Nov 15 2018 at 15:58):

oh, good to know

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 15:58):

yup it is ridiculous how faster 32bits are

view this post on Zulip Karl Palmskog (Nov 15 2018 at 15:59):

sadly these tricks don't seem to be widely known

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 16:01):

Now we have these .aux files, but they are a pain to handle

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 16:02):

time to introduce .vp files

view this post on Zulip Karl Palmskog (Nov 15 2018 at 16:02):

what would they contain?

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Nov 15 2018 at 16:03):

btw @Emilio Jesús Gallego Arias are you coming to CoqPL by any chance?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 16:04):

I will give the invited talk I think

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 16:04):

so yes :D :D

view this post on Zulip Karl Palmskog (Nov 15 2018 at 16:04):

oh great

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 16:04):

I need to book my tickets tho

view this post on Zulip Karl Palmskog (Nov 15 2018 at 16:04):

I will give a talk as well, hope we can chat a bit

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 16:04):

of course!

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 16:04):

fantastic!

view this post on Zulip Karl Palmskog (Nov 15 2018 at 16:04):

we hope to join the consortium quite soon

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Nov 15 2018 at 16:05):

right, I think Zach Tatlock at UW will be in touch with Maxime

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 16:05):

:)

view this post on Zulip Karl Palmskog (Nov 15 2018 at 16:05):

OK thanks again

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2018 at 16:05):

thanks to you!

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Nov 15 2018 at 16:06):

great

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Nov 17 2018 at 04:11):

(for getting a PR merged)

view this post on Zulip Karl Palmskog (Nov 17 2018 at 04:12):

still think having released packages for most contribs/community is a good idea

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Nov 20 2018 at 22:00):

or is there some magic way to get precompiled Coq 8.9 branch?

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Nov 22 2018 at 17:33):

sounds good

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Nov 22 2018 at 17:37):

I think you should open an issue for them, and add the "maintainer-wanted" tag.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Nov 22 2018 at 18:00):

Unfortunately the opening of the issue about Nix will have to wait tomorrow

view this post on Zulip Karl Palmskog (Nov 22 2018 at 18:46):

OK, will open issues then

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 23 2018 at 18:42):

@Karl Palmskog see also dune/dune#1555

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Nov 23 2018 at 19:52):

@Emilio Jesús Gallego Arias does that enable capturing extracted files as well?

view this post on Zulip Karl Palmskog (Nov 23 2018 at 19:53):

sounds great even without that though

view this post on Zulip Anton Trunov (Nov 23 2018 at 19:56):

@Emilio Jesús Gallego Arias coq support in dune! very cool!

view this post on Zulip Emilio Jesús Gallego Arias (Nov 23 2018 at 20:16):

@Karl Palmskog yes we can add an (extracted_modules ...) field for sure

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Nov 23 2018 at 21:05):

for posterity, the right link is ocaml/dune#1555

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Nov 24 2018 at 12:21):

I think it detracts from non-github readability to have a bunch of ", ' and the like

view this post on Zulip Théo Zimmermann (Nov 24 2018 at 12:21):

There is a way to not preprocess : {{& }} (see the use with opam version constraints)

view this post on Zulip Karl Palmskog (Nov 24 2018 at 12:22):

OK, then I think that that should be used for description and documentation at least

view this post on Zulip Théo Zimmermann (Nov 24 2018 at 12:22):

Indeed.

view this post on Zulip Théo Zimmermann (Nov 24 2018 at 12:28):

Feel free to push a commit fixing this without going through a PR.

view this post on Zulip Karl Palmskog (Nov 24 2018 at 12:30):

OK will do

view this post on Zulip 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)"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Dec 05 2018 at 21:37):

a real domain instead of coq-community.github.io would also be nice

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Dec 06 2018 at 21:24):

in my testing I can't really see much of a difference in practice

view this post on Zulip Théo Zimmermann (Dec 10 2018 at 13:16):

a real domain instead of coq-community.github.io would also be nice

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Dec 10 2018 at 13:54):

Then I suppose the author of this is @Enrico Tassi.

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Karl Palmskog (Dec 10 2018 at 23:07):

correction: http://elm-community.org

view this post on Zulip Théo Zimmermann (Dec 11 2018 at 09:20):

Right. I will look into this.

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Dec 14 2018 at 21:43):

maybe only basic static website files + generation scripts in master?

view this post on Zulip Théo Zimmermann (Dec 17 2018 at 15:52):

GitHub pages support both the gh-pages branch setup and the docs/ sub-directory setup.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Dec 17 2018 at 20:05):

I think we should go with docs/ for now then

view this post on Zulip Théo Zimmermann (Dec 18 2018 at 08:23):

:+1:

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Maxime Dénès (Jan 21 2019 at 11:04):

I can try to investigate, indeed

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 15:48):

Cool!

view this post on Zulip Karl Palmskog (Feb 02 2019 at 15:48):

so I think I will do a manifesto PR to enable using identifier

view this post on Zulip Karl Palmskog (Feb 02 2019 at 15:48):

and we should use it when rolling out releases of all Coq-community packages

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 15:48):

Yep, and probably remove the shortname at the same time, right?

view this post on Zulip Karl Palmskog (Feb 02 2019 at 15:49):

yeah probably a good idea

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 02 2019 at 15:49):

(with Coq-community URLs still being default)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 15:53):

Yep, do not hesitate to open issues on the manifesto tracker though.

view this post on Zulip 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...

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Feb 02 2019 at 15:56):

yeah I think that would be great if we can figure out more automation there.

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Feb 02 2019 at 15:56):

advertisement

view this post on Zulip Karl Palmskog (Feb 02 2019 at 15:57):

he had a slide calling for contributors basically

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 15:57):

Advertisement for coq-community specifically or for Coq in general?

view this post on Zulip Karl Palmskog (Feb 02 2019 at 15:57):

for Coq-community

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 15:58):

Hey that's nice! Especially given that he was not so convinced initially :)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Feb 02 2019 at 15:59):

cool, I will try to come as well

view this post on Zulip 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)

view this post on Zulip Karl Palmskog (Feb 02 2019 at 16:01):

until then I'll try to attend the workgroup meetings, although my French is super rusty

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:01):

However, I don't know if it expires.

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:01):

We don't usually speak French during WGs.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Feb 02 2019 at 16:03):

OK that's nice, I try to watch at least some parts

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:07):

Thanks for your active support!

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:08):

I've been looking a bit at your work with Emilio and your UT lab ;-)

view this post on Zulip Karl Palmskog (Feb 02 2019 at 16:08):

without the CI would have been much harder (we were basically working against v8.9)

view this post on Zulip 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)...

view this post on Zulip Karl Palmskog (Feb 02 2019 at 16:09):

I believe I was at UIUC when you were here

view this post on Zulip Karl Palmskog (Feb 02 2019 at 16:09):

and my boss too

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:09):

Ah OK I didn't know your boss had moved recently!

view this post on Zulip Karl Palmskog (Feb 02 2019 at 16:10):

I think he started in 2016

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:10):

Yep, I know and she was my boss at UT Austin

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:11):

(during the second semester, after a strange first semester with the ACL2 team)

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:12):

I had classes with these two :)

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:13):

But Don was a strange guy, I didn't know he had worked with Coq

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:15):

SPLASH looks like something that is a bit at the frontier though.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Feb 02 2019 at 16:16):

yeah OOPSLA may be the best middle ground.

view this post on Zulip 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, ...)

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:21):

I've just submitted a paper to MSR (Mining Software Repositories).

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:21):

This is associated to ICSE.

view this post on Zulip Karl Palmskog (Feb 02 2019 at 16:22):

ah, we've talked about "mining proof repositories" stuff here

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:22):

Ah that's cool. Do you have a pointer?

view this post on Zulip Karl Palmskog (Feb 02 2019 at 16:22):

there are some papers in that direction, like metrics for proofs

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:23):

I would be interested in pointers in research on CI too.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 02 2019 at 16:24):

I can send an email with some stuff

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:24):

Thanks!

view this post on Zulip Karl Palmskog (Feb 02 2019 at 16:24):

I assume the paris-diderot email?

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:24):

Yep, that one is good.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:40):

Yes. And getting "in" supposes having already attained a certain level of maturity.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:41):

Yes, that's why the coq-community project has this idea of an "editorial committee".

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Feb 02 2019 at 16:41):

oh, right, you were thinking of that with Pierre [Casteran] right?

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:42):

Yes, and some others like Bas Spitters.

view this post on Zulip Karl Palmskog (Feb 02 2019 at 16:42):

Jasmin Blanchette says he wants to do an AFP for Lean as well

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:45):

And then, this tight link with the development might make sense.

view this post on Zulip Karl Palmskog (Feb 02 2019 at 16:45):

AFP also fills the function of providing "academic cover" for just doing the actual proof work

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:45):

(like for Coq and its plugins)

view this post on Zulip Karl Palmskog (Feb 02 2019 at 16:45):

one can put in one's CV that project so-and-so got into the archive

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 02 2019 at 16:47):

I think it's both, I know Jasmin tends to emphasize both

view this post on Zulip Karl Palmskog (Feb 02 2019 at 16:47):

like IsaFOL, it's so many papers at this point

view this post on Zulip Karl Palmskog (Feb 02 2019 at 16:48):

so the best single reference is what's in AFP

view this post on Zulip Théo Zimmermann (Feb 02 2019 at 16:51):

Thanks for your mail!

view this post on Zulip Karl Palmskog (Feb 02 2019 at 16:53):

:thumbsup:

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 05 2019 at 22:13):

I think we need some checklist there

view this post on Zulip Karl Palmskog (Feb 05 2019 at 22:55):

oh, that failed too, see email

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Feb 07 2019 at 10:31):

Adam has two accounts. I did not invite his -biz account.

view this post on Zulip Karl Palmskog (Feb 07 2019 at 14:29):

:thumbsup:

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Feb 07 2019 at 21:13):

ok

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Feb 07 2019 at 21:17):

cool :+1:

view this post on Zulip Karl Palmskog (Feb 07 2019 at 21:17):

basically, most unkilled mutants are not bugs but kind of about dangling definitions

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 07 2019 at 21:18):

but it depends on the context

view this post on Zulip Théo Zimmermann (Feb 07 2019 at 21:19):

What about unused lemmas? Are they flagged too?

view this post on Zulip Karl Palmskog (Feb 07 2019 at 21:19):

we didn't mutate lemma statements this time

view this post on Zulip Karl Palmskog (Feb 07 2019 at 21:20):

might be better to use something like dpdgraph there

view this post on Zulip Théo Zimmermann (Feb 07 2019 at 21:20):

I see

view this post on Zulip Karl Palmskog (Feb 07 2019 at 21:21):

but it may make sense for some projects

view this post on Zulip Karl Palmskog (Feb 07 2019 at 21:21):

I just couldn't find a good way to justify it in the paper

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Feb 08 2019 at 15:47):

He won't mind.

view this post on Zulip Karl Palmskog (Feb 10 2019 at 02:18):

I think it's time to write a template for OPAM2 files

view this post on Zulip Karl Palmskog (Feb 10 2019 at 02:18):

some packages should probably go into extra-dev

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Feb 10 2019 at 17:14):

yeah I heard that. We could always have some convention like <name>.opam2.

view this post on Zulip Karl Palmskog (Feb 10 2019 at 17:15):

the annoying thing about opam2 is they have both a synopsis and description field

view this post on Zulip Karl Palmskog (Feb 10 2019 at 17:16):

I'm not sure either of them can/should contain Markdown

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 10 2019 at 17:46):

then we just use the description field from meta.yml as is

view this post on Zulip Karl Palmskog (Feb 10 2019 at 17:47):

maybe one could automate synchronizing repo descriptions with synopsis at some point

view this post on Zulip Théo Zimmermann (Feb 10 2019 at 19:56):

:+1: sounds doable

view this post on Zulip Karl Palmskog (Feb 16 2019 at 23:17):

OPAM2 migration heating up: https://github.com/coq/opam-coq-archive/pull/587

view this post on Zulip Karl Palmskog (Feb 19 2019 at 18:53):

so it seems like an odious requirement to not have OCaml warnings in old plugins

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2019 at 18:54):

What do you mean @Karl Palmskog ?

view this post on Zulip Karl Palmskog (Feb 19 2019 at 18:54):

I would be in favor of not having such Coq-community plugins in Coq's CI

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2019 at 18:54):

why is it odious?

view this post on Zulip Karl Palmskog (Feb 19 2019 at 18:54):

I mean, assume maintainership and suddenly you have to refactor a lot of internals

view this post on Zulip Karl Palmskog (Feb 19 2019 at 18:54):

even though the plugin works

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2019 at 18:55):

for example with the merge of primitive integers

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2019 at 18:56):

also disabling warnings in your plugin is usually OK

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 19 2019 at 18:56):

the aac-tactics warnings have been around for ages and are all over the codebase

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2019 at 18:57):

let me look into that one

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2019 at 18:57):

we can of course disable that warning for acc-tactics

view this post on Zulip Théo Zimmermann (Feb 19 2019 at 18:57):

it would be great to actually find which warnings are the most pressing to fix

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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"...

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Feb 19 2019 at 18:59):

not a real critic, I have done the same thing in the past

view this post on Zulip Théo Zimmermann (Feb 19 2019 at 18:59):

with warnings too

view this post on Zulip Karl Palmskog (Feb 19 2019 at 18:59):

so I can plan to spend time

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2019 at 19:01):

yeah see my comments here https://github.com/QuickChick/QuickChick/issues/143

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2019 at 19:02):

acc-tactics dies on an comment warning

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2019 at 19:02):

these ones are trivial to fix

view this post on Zulip Karl Palmskog (Feb 19 2019 at 19:07):

sure, but there are lots of incomplete matching warnings

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2019 at 19:08):

let me check a non failing build

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2019 at 19:09):

where do you see them?

view this post on Zulip Karl Palmskog (Feb 19 2019 at 19:27):

OK maybe I mixed it up with some other plugin, or some Coq level warning

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Mar 03 2019 at 22:03):

nice

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Mar 04 2019 at 16:16):

We only have 122 users so far.

view this post on Zulip Karl Palmskog (Mar 04 2019 at 17:01):

:thumbsup:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Mar 08 2019 at 10:03):

None of them have Travis enable. Let me change this.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Mar 08 2019 at 12:58):

:thumbsup:

view this post on Zulip Karl Palmskog (Mar 11 2019 at 16:04):

one thing that's missing now is to write a converter from description to meta.yml

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Mar 12 2019 at 21:21):

sure, I took the best approximation, the license in description was already inconsistent with LICENSE

view this post on Zulip Karl Palmskog (Mar 12 2019 at 21:22):

@Théo Zimmermann so what string should we use for public domain then, as a policy?

view this post on Zulip Karl Palmskog (Mar 12 2019 at 21:23):

I would generally vote for "relicensing" under Unlicense

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Mar 14 2019 at 09:37):

:+1:

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Mar 15 2019 at 00:22):

I would say as soon as the OPAM repo migrates to OPAM2

view this post on Zulip Théo Zimmermann (Mar 15 2019 at 11:05):

There are two cases to consider though:

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Mar 15 2019 at 14:49):

I think many (most?) 8.8 packages are incompatible due to the Implicit Arguments deprecation

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Mar 15 2019 at 15:37):

... only give nudges, such as saying that it will save time, etc.

view this post on Zulip 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...

view this post on Zulip Karl Palmskog (Mar 16 2019 at 00:14):

with coq-<shortname>.opam one can do opam pin add coq-<shortname> . in CI

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Mar 17 2019 at 22:12):

hmm, I think the Cachix-Coq is stale: https://github.com/coq/coq-on-cachix

view this post on Zulip Karl Palmskog (Mar 17 2019 at 22:12):

not updated for 7 days

view this post on Zulip Karl Palmskog (Mar 17 2019 at 22:12):

this makes CI fail for my nice plugin port to handle SProp changes...

view this post on Zulip Théo Zimmermann (Mar 18 2019 at 08:57):

fixed

view this post on Zulip Karl Palmskog (Mar 18 2019 at 14:57):

:thumbsup:

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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/

view this post on Zulip Théo Zimmermann (Mar 24 2019 at 17:38):

:+1:

view this post on Zulip 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.)

view this post on Zulip Karl Palmskog (Apr 03 2019 at 16:53):

or what do you think?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 16:55):

opam pin add dune --dev allows you to test that now

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Apr 03 2019 at 16:56):

and the PR target is configurable?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 16:56):

that's my question, in the past it was

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 16:57):

so it shouldn't be too hard

view this post on Zulip Karl Palmskog (Apr 03 2019 at 16:57):

so maybe the main drawback is that the project has to be dunerized?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 16:58):

yes it is designed for that

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 16:58):

you can use opam-publish / topkg otherwise

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 16:58):

I dunno if anyone has written support for coq_makefile

view this post on Zulip Karl Palmskog (Apr 03 2019 at 16:58):

OK, then I would probably vote for aiming to use that for 8.10 releases

view this post on Zulip Karl Palmskog (Apr 03 2019 at 16:58):

and use opam-publish for now

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 16:59):

it is experimental of course, but if anyone is interested

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Apr 03 2019 at 16:59):

am interested but it should probably be tried on some small project

view this post on Zulip Karl Palmskog (Apr 03 2019 at 16:59):

is the Coq support in 1.9 as well?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 16:59):

basically I had never to care about things

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 16:59):

yup

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:00):

sorry, the Coq support is what is in 1.9

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:00):

dune-release has been there since a lot

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:00):

so with Dune 1.9

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:01):

provided there are no bugs or course :crossed_flags:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:04):

https://dune.readthedocs.io/en/latest/coq.html

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:04):

of course improvements welcome

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:04):

pity in discouse it seems we cannot assign a post to two categories

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:05):

also Dune release notes will contaian a small example

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:05):

https://coq.github.io/doc/master/refman/practical-tools/utilities.html#building-a-coq-project-with-dune

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:05):

?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:06):

_CoqProject is not taken into account

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:06):

it takes care of it

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:06):

maybe should be in the F.A.Q.

view this post on Zulip Karl Palmskog (Apr 03 2019 at 17:06):

but what about CoqIDE/ProofGeneral?

view this post on Zulip Karl Palmskog (Apr 03 2019 at 17:06):

I just want to clone a project, build it, then start to modify files

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:07):

Oh good point, I guess I should submit a PR to GP

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:07):

to PG

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:07):

as for CoqIDE

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:07):

I dunno

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:07):

indeed that's a todo

view this post on Zulip Karl Palmskog (Apr 03 2019 at 17:07):

so then one should arguably: delete the file list from _CoqProject, but keep the flags

view this post on Zulip Karl Palmskog (Apr 03 2019 at 17:07):

for compatibility

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Apr 03 2019 at 17:08):

oh, so .vo files end up somewhere else

view this post on Zulip Karl Palmskog (Apr 03 2019 at 17:09):

then you really need that PG patch

view this post on Zulip Karl Palmskog (Apr 03 2019 at 17:10):

I think it's a very common workflow to clone + build + open file in emacs/PG

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:17):

Yes keeping a Makefile as a wrapper is customary

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:19):

needs more discussion as merlin / OCaml people are implementhing heavier protocols for this

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 17:19):

But you are right for now I've only worried about batch-building

view this post on Zulip Karl Palmskog (Apr 03 2019 at 17:20):

so flags like -arg -w -arg -notation-overridden are handled by dune as well, right?

view this post on Zulip Karl Palmskog (Apr 03 2019 at 17:20):

I think we need a way to communicate those to PG/CoqIDE

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Apr 03 2019 at 17:21):

for dependency management

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Apr 03 2019 at 17:31):

so you might want to use dune for batch-building and installs

view this post on Zulip Karl Palmskog (Apr 03 2019 at 17:32):

I also want to look at the extraction story

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Apr 03 2019 at 17:34):

with .vo files hygienized the extraction build rules won't work

view this post on Zulip Karl Palmskog (Apr 03 2019 at 17:35):

installing is not the only goal of building

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Apr 03 2019 at 19:20):

per the manual, there is no way to use -Q in coq-dune?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 20:08):

What does "using -Q" mean?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 20:09):

however when depending on them they will be targetted with -Q

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 20:09):

so they are wrapped

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 20:09):

this needs refinement in the next PR

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2019 at 20:10):

I'll open an issue about that actually

view this post on Zulip Karl Palmskog (Apr 03 2019 at 21:06):

OK I see

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2019 at 15:00):

@Karl Palmskog can you open an issue about extraction support in Dune ? Thanks!

view this post on Zulip Karl Palmskog (Apr 04 2019 at 16:34):

@Emilio Jesús Gallego Arias will do

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2019 at 16:56):

thanks @Karl Palmskog

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip Anton Trunov (Apr 12 2019 at 14:19):

Makes sense, @Emilio Jesús Gallego Arias. Keeping my fingers crossed :)

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Apr 15 2019 at 08:09):

Obviously, this is a hack until there is better editor support.

view this post on Zulip 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

view this post on Zulip Anton Trunov (Apr 15 2019 at 09:58):

@Théo Zimmermann @Emilio Jesús Gallego Arias Thank you both for your suggestion!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (May 04 2019 at 10:37):

:+1:

view this post on Zulip Karl Palmskog (May 15 2019 at 22:45):

is there a way to test w/ 8.10 branch and/or beta in Nix?

view this post on Zulip Karl Palmskog (May 16 2019 at 01:08):

ah, saw at least how to do the 8.10 branch

view this post on Zulip Karl Palmskog (May 17 2019 at 02:04):

I did all the releases and package submissions for the projects I maintain, was fairly quick

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (May 17 2019 at 20:20):

would be useful for us to get them "timestamped"

view this post on Zulip Théo Zimmermann (May 18 2019 at 14:50):

I don't think he would mind.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (May 18 2019 at 15:33):

OK, I'll make do with v8.10 in Nix for now

view this post on Zulip Théo Zimmermann (May 22 2019 at 18:39):

FWIW 8.10+beta1 is in nixpkgs-unstable now.

view this post on Zulip Karl Palmskog (May 22 2019 at 18:45):

@Théo Zimmermann so this mean I can just use8.10+beta1 in meta.yml?

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (May 22 2019 at 19:12):

OK great

view this post on Zulip Karl Palmskog (May 22 2019 at 19:13):

now I just need 8.10 Docker image and my life would be (nearly) complete

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (May 22 2019 at 19:17):

it would probably be something like 1 primary + n secondary + m extraction

view this post on Zulip Théo Zimmermann (May 22 2019 at 19:17):

I have an example in mind which is coq-community projects zorns-lemma + topology

view this post on Zulip Karl Palmskog (May 22 2019 at 19:18):

yeah we should fix those templates to at least be up to date first though

view this post on Zulip Théo Zimmermann (May 22 2019 at 19:18):

I had a PR opened about this

view this post on Zulip Théo Zimmermann (May 22 2019 at 19:18):

two actually, although I think one of them needed some changes

view this post on Zulip 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

view this post on Zulip Karl Palmskog (May 22 2019 at 19:19):

I think that can happen with extraction as well

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (May 22 2019 at 19:20):

That would be a good step forward indeed.

view this post on Zulip Karl Palmskog (May 22 2019 at 19:21):

figuring out boilerplate has taken me huge effort over time

view this post on Zulip Théo Zimmermann (May 22 2019 at 19:21):

Yep, and everyone has to figure the same thing over and over

view this post on Zulip 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

view this post on Zulip Karl Palmskog (May 22 2019 at 19:22):

it was nearly always possible to override the "biased" defaults

view this post on Zulip 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 ;-)

view this post on Zulip Karl Palmskog (May 22 2019 at 19:22):

but you had to be sufficiently bothered by them

view this post on Zulip Karl Palmskog (May 22 2019 at 19:23):

yeah I saw that they're merging dune-release into dune, that's very Rails-y

view this post on Zulip Théo Zimmermann (May 22 2019 at 19:24):

Are they?

view this post on Zulip Karl Palmskog (May 22 2019 at 19:25):

https://github.com/ocaml/dune/issues/2171

view this post on Zulip 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...

view this post on Zulip Karl Palmskog (May 22 2019 at 19:27):

or what do you think?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (May 22 2019 at 19:28):

Or issue?

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (May 22 2019 at 19:29):

We can discuss about the right strategy for this in Sophia I guess.

view this post on Zulip Karl Palmskog (May 22 2019 at 19:30):

agree

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Karl Palmskog (May 22 2019 at 19:35):

I have an absurdly long PDF (25+ pages) going through live mutants

view this post on Zulip Théo Zimmermann (May 22 2019 at 19:36):

?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Théo Zimmermann (May 22 2019 at 19:38):

sorry I'm a bit unclear on the terminology

view this post on Zulip Théo Zimmermann (May 22 2019 at 19:38):

what do you call a "live mutant" again?

view this post on Zulip Karl Palmskog (May 22 2019 at 19:38):

killed mutant: a project is modified and some proof fails

view this post on Zulip Karl Palmskog (May 22 2019 at 19:38):

live mutant: a project is modified and all proofs pass

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (May 22 2019 at 19:42):

we can't advertise widely since we're in double-blind review

view this post on Zulip Karl Palmskog (May 22 2019 at 19:43):

we explained to Georges in an email, so he knows

view this post on Zulip Théo Zimmermann (May 22 2019 at 19:43):

oh well...

view this post on Zulip Théo Zimmermann (May 22 2019 at 19:43):

double-blind... sigh!

view this post on Zulip Karl Palmskog (May 22 2019 at 19:43):

I'm going to implement his suggestions and we can claim "PR accepted" and so on

view this post on Zulip Karl Palmskog (May 22 2019 at 19:44):

yeah, people reporting bugs are hardest hit

view this post on Zulip Karl Palmskog (May 22 2019 at 19:44):

some have to use dummy GitHub accounts

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (May 22 2019 at 19:45):

If people look for who did this migration, they can find out.

view this post on Zulip Théo Zimmermann (May 22 2019 at 19:45):

But still the committees of two conferences did not complain.

view this post on Zulip Karl Palmskog (May 22 2019 at 19:46):

yes, it's a gray area

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (May 22 2019 at 19:46):

So if people do, it's their fault.

view this post on Zulip Théo Zimmermann (May 22 2019 at 19:46):

Previous versions of my paper were also on HAL anyway.

view this post on Zulip Karl Palmskog (May 22 2019 at 19:46):

some PC chairs would not be content with that...

view this post on Zulip Karl Palmskog (May 22 2019 at 19:47):

but you never know

view this post on Zulip Théo Zimmermann (May 22 2019 at 19:47):

with which part?

view this post on Zulip Karl Palmskog (May 22 2019 at 19:47):

referencing a repo that can be used to find out identities

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (May 22 2019 at 19:48):

and if reviewers are looking too much, they can find out identities for sure

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jul 12 2019 at 17:32):

I think we may need some dictionary, "principal maintainer" vs. "Coq-community maintainer"

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Jul 12 2019 at 17:36):

I guess the opposite order may be preferred

view this post on Zulip 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"?

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Jul 12 2019 at 18:58):

what would we call such non-principal maintainers for precision?

view this post on Zulip Théo Zimmermann (Jul 12 2019 at 19:37):

What about just "coq-community members"? See also coq-community/manifesto#77.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jul 13 2019 at 16:20):

@Anton Trunov OK I guess we'll wait a few days more then

view this post on Zulip 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?

view this post on Zulip 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/

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Aug 15 2019 at 18:33):

will just create an issue to collect links and resources

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Anton Trunov (Aug 21 2019 at 16:32):

And perhaps extraction tag could be added as well

view this post on Zulip 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.

view this post on Zulip Anton Trunov (Aug 21 2019 at 17:14):

That’s correct, it’s for manifesto repository.

view this post on Zulip 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.

view this post on Zulip Anton Trunov (Aug 21 2019 at 17:15):

OK, I’ll add the tags you suggested. Thanks

view this post on Zulip Anton Trunov (Aug 21 2019 at 17:15):

in any case, it would be good if we invented tags so that all move-project have one tag.

could you expand a bit on this?

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Aug 21 2019 at 17:17):

since we have like a bunch of them

view this post on Zulip Anton Trunov (Aug 21 2019 at 17:18):

you mean in addition to move-project, right?

view this post on Zulip Karl Palmskog (Aug 21 2019 at 17:19):

yes

view this post on Zulip Karl Palmskog (Aug 21 2019 at 17:19):

or do you mean we replace move-project with move-coq-plugin, etc.?

view this post on Zulip Anton Trunov (Aug 21 2019 at 17:19):

hmmm, now you got me thinking

view this post on Zulip Anton Trunov (Aug 21 2019 at 17:20):

https://github.com/coq-community/manifesto/labels/maintainer-wanted

view this post on Zulip Anton Trunov (Aug 21 2019 at 17:20):

I started adding more labels

view this post on Zulip Anton Trunov (Aug 21 2019 at 17:20):

but we can change that

view this post on Zulip Karl Palmskog (Aug 21 2019 at 17:20):

I think what you've added there works well

view this post on Zulip 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

view this post on Zulip Anton Trunov (Aug 21 2019 at 17:27):

ok, I added some more tags to accompany move-project, except for VsCoq

view this post on Zulip Anton Trunov (Aug 21 2019 at 17:27):

coq-ide or just external-tool (or both)?

view this post on Zulip Karl Palmskog (Aug 21 2019 at 17:28):

maybe just external-tool for now

view this post on Zulip Anton Trunov (Aug 21 2019 at 17:28):

oops, I forgot to clear is: open

view this post on Zulip Karl Palmskog (Aug 21 2019 at 17:28):

then you capture ProViola as well

view this post on Zulip Anton Trunov (Aug 21 2019 at 17:28):

ok

view this post on Zulip Karl Palmskog (Aug 21 2019 at 17:28):

we can rename later

view this post on Zulip Anton Trunov (Aug 21 2019 at 17:33):

ok, I’m done this time, feel free to make edits

view this post on Zulip 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 ;-)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Aug 30 2019 at 08:36):

@Maxime Dénès For sure!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Aug 30 2019 at 11:25):

indeed

view this post on Zulip 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)

view this post on Zulip Karl Palmskog (Sep 03 2019 at 02:31):

as soon as he asked for LinkedIn profile and code examples the guy went silent

view this post on Zulip Karl Palmskog (Sep 03 2019 at 03:00):

some vetting process for changing maintainers of more "important" Coq-community projects may be called for

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Sep 03 2019 at 09:52):

Keybase sounds like a good start, let's discuss in the near future

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Anton Trunov (Sep 19 2019 at 16:02):

Great idea! I hope the authors of unmaintained projecs will agree to merge such PRs :)

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Oct 08 2019 at 21:29):

I don't think they would mind, no.

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip Gregory Malecha (Oct 16 2019 at 17:27):

make INSTALLDIR=?

view this post on Zulip Gregory Malecha (Oct 16 2019 at 17:27):

or something like that

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Guillaume Claret (Gitter import) (Nov 05 2019 at 09:39):

:+1:

view this post on Zulip Anton Trunov (Dec 07 2019 at 19:19):

Does anyone know why recently builds on coq-on-cachix fail?

view this post on Zulip Anton Trunov (Dec 07 2019 at 19:19):

e.g. https://travis-ci.com/coq-community/lemma-overloading/jobs/264348908?utm_medium=notification&utm_source=email

view this post on Zulip Anton Trunov (Dec 07 2019 at 19:20):

opam builds on the other hand succeed

view this post on Zulip Karl Palmskog (Dec 07 2019 at 19:22):

there's something wrong with ssreflect and Nix

view this post on Zulip Karl Palmskog (Dec 07 2019 at 19:22):

on 8.11 and master, but not 8.10

view this post on Zulip Karl Palmskog (Dec 07 2019 at 19:22):

I have no idea why

view this post on Zulip 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

view this post on Zulip Anton Trunov (Dec 07 2019 at 19:31):

yeah, me neither

view this post on Zulip Karl Palmskog (Dec 07 2019 at 19:33):

@Anton Trunov btw, any 1.10 release of fcsl-pcm in the works?

view this post on Zulip Karl Palmskog (Dec 07 2019 at 19:34):

it's going to be compatibility-breaking, right? No Coq 8.9?

view this post on Zulip Anton Trunov (Dec 07 2019 at 19:34):

oh yeah, I’ll try to do it later next week

view this post on Zulip 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)

view this post on Zulip Anton Trunov (Dec 07 2019 at 19:41):

:thumbsup:

view this post on Zulip 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)

view this post on Zulip Gregory Malecha (Dec 11 2019 at 20:30):

@Karl Palmskog it sounds like we just need quotients, then all is easy :-)

view this post on Zulip Karl Palmskog (Dec 13 2019 at 09:21):

if only

view this post on Zulip 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/

view this post on Zulip Karl Palmskog (Dec 27 2019 at 15:20):

structure shamelessly borrowed from MathComp

view this post on Zulip Anton Trunov (Dec 27 2019 at 16:44):

@Karl Palmskog Looks awesome! Is there any documentation describing the workflow?

view this post on Zulip Karl Palmskog (Dec 27 2019 at 16:53):

@Anton Trunov not yet, working on it, will probably be documented in the wiki

view this post on Zulip Anton Trunov (Dec 27 2019 at 16:54):

cool! you mean the manifesto wiki, right?

view this post on Zulip Karl Palmskog (Dec 27 2019 at 16:54):

right

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Karl Palmskog (Dec 27 2019 at 17:10):

my friend is helping out with fixing some annoying things about coqdocjs

view this post on Zulip Karl Palmskog (Dec 27 2019 at 17:10):

so the website will probably improve in a few hours

view this post on Zulip Théo Zimmermann (Dec 27 2019 at 17:10):

:+1:

view this post on Zulip Guillaume Claret (Gitter import) (Dec 27 2019 at 17:46):

:+1:

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Dec 27 2019 at 18:24):

spacing between lemmas looks better and I added the missing Proof. for Defined stuff

view this post on Zulip Karl Palmskog (Dec 27 2019 at 18:27):

good enough to implement for lemma-overloading etc., or what do you think @Anton Trunov ?

view this post on Zulip Anton Trunov (Dec 27 2019 at 18:35):

@Karl Palmskog I think so. Btw, it would be great to have deployment automated.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Jan 01 2020 at 13:39):

we could try to contribute stuff upstream but not be dependent on it

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 02 2020 at 09:37):

for example, footer links to coq-community, Makefile tasks assume one follows conventions

view this post on Zulip Karl Palmskog (Jan 02 2020 at 09:38):

and instructions are getting quite non-general at this point (assumes GitHub pages are used)

view this post on Zulip Karl Palmskog (Jan 02 2020 at 09:38):

I guess I could start an issue and ask tebbi what he prefers

view this post on Zulip 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...

view this post on Zulip Karl Palmskog (Jan 02 2020 at 09:40):

well, the core scripts are essentially the same (although that may change)

view this post on Zulip Karl Palmskog (Jan 02 2020 at 09:41):

but basically everything else is different

view this post on Zulip Karl Palmskog (Jan 02 2020 at 09:41):

so it will be quite a hassle to maintain on top of existing coqdocjs

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Karl Palmskog (Jan 02 2020 at 09:45):

too much work for me, this is already way over my time budget

view this post on Zulip 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...

view this post on Zulip Karl Palmskog (Jan 02 2020 at 09:51):

:thumbsup:

view this post on Zulip Karl Palmskog (Jan 02 2020 at 10:21):

ok done as coq-community/manifesto#88

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 02 2020 at 12:41):

I might start one for HOL4 just for fun

view this post on Zulip Karl Palmskog (Jan 04 2020 at 20:30):

https://github.com/coq-community/manifesto/wiki/Generating-and-deploying-coqdoc-HTML-documentation

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip Anton Trunov (Jan 04 2020 at 20:58):

And kudos for documenting how to use coqdoc!

view this post on Zulip Karl Palmskog (Jan 04 2020 at 20:59):

maybe one try to ping the other guy doing awesome-coq in his own account

view this post on Zulip Karl Palmskog (Jan 04 2020 at 21:01):

coqdoc can do nice stuff but it's arguably undermaintained

view this post on Zulip Karl Palmskog (Jan 04 2020 at 21:01):

for example I reported the serious bug which makes all sentences with annotations disappear

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Anton Trunov (Jan 04 2020 at 21:13):

@Théo Zimmermann @Karl Palmskog what do you think?

view this post on Zulip 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

view this post on Zulip Anton Trunov (Jan 04 2020 at 21:24):

ok, here is the issue https://github.com/uhub/awesome-coq/issues/11

view this post on Zulip Karl Palmskog (Jan 04 2020 at 21:35):

:thumbsup:

view this post on Zulip 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.

view this post on Zulip Anton Trunov (Jan 04 2020 at 21:38):

I’ve noticed Programs and Proofs by I. Sergey there

view this post on Zulip Karl Palmskog (Jan 04 2020 at 21:41):

right, but that's arguably a Coq project too

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 09 2020 at 09:48):

the OCaml one is a good template

view this post on Zulip Anton Trunov (Jan 09 2020 at 10:55):

@Karl Palmskog Sounds good!

view this post on Zulip Karl Palmskog (Jan 09 2020 at 11:15):

the main work may be to get it listed in all other awesome lists

view this post on Zulip Anton Trunov (Jan 09 2020 at 11:16):

that’s for sure the biggest challenge :)

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Jan 09 2020 at 17:52):

they have some nice OCaml image for awesome-ocaml, that would be a nice equivalent

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 09 2020 at 19:25):

I guess I can/will also catch flak for headings/subject division

view this post on Zulip Emilio Jesús Gallego Arias (Jan 09 2020 at 20:16):

very nice folks, congrats!!

view this post on Zulip Emilio Jesús Gallego Arias (Jan 09 2020 at 20:17):

should it be added to Coq's README / webpage?

view this post on Zulip Karl Palmskog (Jan 09 2020 at 20:20):

I think we should wait for more opinions/PRs

view this post on Zulip 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...

view this post on Zulip Karl Palmskog (Jan 09 2020 at 21:19):

there should probably be a "Framework" section for Bedrock2, Fiat, Iris, Verdi, VST

view this post on Zulip Karl Palmskog (Jan 09 2020 at 21:35):

and Disel, Aneris

view this post on Zulip 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?

view this post on Zulip Anton Trunov (Jan 09 2020 at 21:41):

I can ask Ilya about that

view this post on Zulip Karl Palmskog (Jan 09 2020 at 21:42):

:thumbsup:

view this post on Zulip Anton Trunov (Jan 09 2020 at 21:42):

But first, do we not want to reuse coq-community’s logo?

view this post on Zulip Anton Trunov (Jan 09 2020 at 21:42):

CC @Théo Zimmermann

view this post on Zulip Karl Palmskog (Jan 09 2020 at 21:42):

I mean, the list is not about coq-community

view this post on Zulip Anton Trunov (Jan 09 2020 at 21:42):

fair enough

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 09 2020 at 21:43):

OK

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Anton Trunov (Jan 09 2020 at 22:17):

btw, looks like awesome-ocaml reuses the OCaml logo

view this post on Zulip Karl Palmskog (Jan 09 2020 at 22:23):

sure, but the Coq logo is not nice to look at

view this post on Zulip Karl Palmskog (Jan 09 2020 at 22:47):

note to self: add Coq OPAM repo ref under Package Management

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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")

view this post on Zulip Théo Zimmermann (Jan 10 2020 at 10:00):

It is a bit weird that "coq-community" is missing from the Community section...

view this post on Zulip 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).

view this post on Zulip Théo Zimmermann (Jan 10 2020 at 10:03):

There is also a non-official IRC

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Théo Zimmermann (Jan 10 2020 at 10:07):

I feel this is missing a "Verified Libraries" section.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Jan 10 2020 at 10:09):

And UniMath should be listed in the "Mathematics" section.

view this post on Zulip Karl Palmskog (Jan 10 2020 at 10:27):

many points raised above are fixed by Anton's PR which I'll merge very soon

view this post on Zulip Karl Palmskog (Jan 10 2020 at 10:27):

.

view this post on Zulip 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

view this post on Zulip Anton Trunov (Jan 10 2020 at 13:25):

@Karl Palmskog looks awesome :)

view this post on Zulip 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/

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Jan 10 2020 at 19:52):

I have some changes standing by until Anton confirms the license.

view this post on Zulip Karl Palmskog (Jan 10 2020 at 19:53):

so please don't tweet just yet

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2020 at 19:57):

Twitter is a wild place tho :)

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2020 at 20:00):

it depends on your "community"

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2020 at 20:00):

for me it is by far the preferred professional network these days

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2020 at 20:00):

I was kinda joking about the wild place

view this post on Zulip 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"

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2020 at 20:01):

"some random folk sees my piece, posts it, gets 100K RTs"

view this post on Zulip Karl Palmskog (Jan 10 2020 at 20:01):

personally I don't like the mix of professional and politics

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2020 at 20:01):

xD

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2020 at 20:01):

Ah, politics.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2020 at 20:02):

yeah, the mix is a problem

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2020 at 20:02):

somehow my stream looks pretty good tho

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2020 at 20:02):

I get the occasional politics things, but mostly about interesting CS stuff

view this post on Zulip Karl Palmskog (Jan 10 2020 at 20:03):

you see someone you respect professionally, and then find out viewpoint differences are fundamental and irreconcilable

view this post on Zulip 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+

view this post on Zulip Karl Palmskog (Jan 10 2020 at 20:03):

ignorance is bliss in most cases

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2020 at 20:04):

overall far from perfect but I get a positive return from twitter

view this post on Zulip 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...

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2020 at 20:05):

are pretty much a political aspect of my professional job

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2020 at 20:05):

and many other stuff I'll skip but relevant to France

view this post on Zulip Karl Palmskog (Jan 10 2020 at 20:05):

this is not where people usually stay

view this post on Zulip Karl Palmskog (Jan 10 2020 at 20:06):

if it was mostly about open source/access, it'd be fine

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2020 at 20:06):

I used to say that universities are just advanced training camps for politicians

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2020 at 20:06):

well that's just an example

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2020 at 20:06):

of course things can go further beyond

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2020 at 20:06):

on the other hand isn't it working as intended?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Jan 10 2020 at 20:13):

hmm, I don't think there is

view this post on Zulip Karl Palmskog (Jan 10 2020 at 20:13):

I'd prefer some kind of decentralized, crypto-based stuff

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 10 2020 at 20:22):

at least if one can do broadcast crypto you can control who gets to read something

view this post on Zulip 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 :)

view this post on Zulip Karl Palmskog (Jan 10 2020 at 20:49):

:thumbsup:

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 10 2020 at 20:50):

OK I pushed a version with LICENSE and stuff

view this post on Zulip Karl Palmskog (Jan 10 2020 at 20:51):

can for sure be tweeted out

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 10 2020 at 20:53):

do we have a coq-community twitter? news to me...

view this post on Zulip Karl Palmskog (Jan 10 2020 at 20:53):

ah didn't see issue

view this post on Zulip Karl Palmskog (Jan 10 2020 at 21:25):

hmm, having a logo is a requirement for getting into the main "awesome"

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Jan 10 2020 at 22:02):

well, you can do it unless you want to try to edit the coq-community svg

view this post on Zulip Karl Palmskog (Jan 10 2020 at 22:03):

I think either is fine as right aligned like the example

view this post on Zulip Karl Palmskog (Jan 11 2020 at 12:14):

HoTT builds documentation for every commit, which has made their repo very inconvenient to clone

view this post on Zulip Karl Palmskog (Jan 11 2020 at 12:15):

took me several minutes last time, and takes several hundred MB on disk

view this post on Zulip 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"

view this post on Zulip Karl Palmskog (Jan 11 2020 at 12:19):

or what do you think @Anton Trunov @Théo Zimmermann ?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jan 12 2020 at 22:03):

:thumbsup:

view this post on Zulip Karl Palmskog (Jan 12 2020 at 22:03):

very, very nice

view this post on Zulip Karl Palmskog (Jan 12 2020 at 22:03):

that painting is just an overall joy to look at

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 13 2020 at 00:33):

compare: https://github.com/coq-community/awesome-coq/tree/add-logo

view this post on Zulip Karl Palmskog (Jan 13 2020 at 00:34):

here's the recommended style: https://github.com/dhamaniasad/awesome-postgres/blob/master/README.md

view this post on Zulip 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:

view this post on Zulip Anton Trunov (Jan 13 2020 at 08:06):

thanks for your edits, btw

view this post on Zulip Karl Palmskog (Jan 13 2020 at 08:37):

https://github.com/sindresorhus/awesome/blob/master/pull_request_template.md

view this post on Zulip Karl Palmskog (Jan 13 2020 at 08:37):

there's a bullet about logos there

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 13 2020 at 09:51):

the problem with 10% is that it can look terrible with non-svg images

view this post on Zulip Karl Palmskog (Jan 13 2020 at 09:52):

depending on resolution and so on

view this post on Zulip 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

view this post on Zulip Anton Trunov (Jan 13 2020 at 10:10):

Oh, I see. Your choice then, I have no working experience in this area :)

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 13 2020 at 10:41):

I think we tick all the awesome list boxes except for "30 days from creation" now

view this post on Zulip Anton Trunov (Jan 13 2020 at 10:46):

:+1:

view this post on Zulip Karl Palmskog (Jan 13 2020 at 10:47):

oh man I was looking up CertikOS stuff

view this post on Zulip Karl Palmskog (Jan 13 2020 at 10:47):

there's basically almost nothing public anymore w.r.t. source code

view this post on Zulip Karl Palmskog (Jan 13 2020 at 10:47):

if there ever was anything...

view this post on Zulip Karl Palmskog (Jan 13 2020 at 10:48):

at least my view is that public source should be available...

view this post on Zulip Karl Palmskog (Jan 13 2020 at 10:51):

(for addition to awesome-coq)

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 13 2020 at 10:54):

right, probably reserved for startup: https://www.certik.org/#home

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 13 2020 at 10:58):

founders win, almost everyone else loses

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jan 13 2020 at 11:44):

What about making "the Coq proof assistant" a clickable link in the top description?

view this post on Zulip Théo Zimmermann (Jan 13 2020 at 12:01):

OK fixed by PR!

view this post on Zulip Anton Trunov (Jan 13 2020 at 12:02):

:+1:

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jan 13 2020 at 12:05):

User Interfaces is sorted under "I", as it was in the OCaml list

view this post on Zulip Karl Palmskog (Jan 13 2020 at 12:05):

but feel free to call it "Interfaces" or move it to the bottom

view this post on Zulip Théo Zimmermann (Jan 13 2020 at 12:06):

Ah... OK.

view this post on Zulip 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?

view this post on Zulip Anton Trunov (Jan 13 2020 at 12:09):

yeah, sometimes it’s hard to classify things, but feel free to propose changes

view this post on Zulip Théo Zimmermann (Jan 13 2020 at 12:09):

:+1:

view this post on Zulip Karl Palmskog (Jan 13 2020 at 12:09):

lumping vs. splitting, indeed super hard

view this post on Zulip 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

view this post on Zulip Anton Trunov (Jan 13 2020 at 12:10):

I second that

view this post on Zulip Anton Trunov (Jan 13 2020 at 12:10):

tagging as in org files usually works great

view this post on Zulip Théo Zimmermann (Jan 13 2020 at 12:12):

Should CFML be added somewhere? Should it go into "Framework" or into "Tools"?

view this post on Zulip Anton Trunov (Jan 13 2020 at 12:12):

I guess “Tools” would be better, since it’s kind of related to CoqOfOCaml

view this post on Zulip Théo Zimmermann (Jan 13 2020 at 12:13):

Yeah, I was thinking the same.

view this post on Zulip Anton Trunov (Jan 13 2020 at 12:13):

and yes, CFML should be added, imho

view this post on Zulip Théo Zimmermann (Jan 13 2020 at 12:13):

I can open a PR for this one and Freespec too.

view this post on Zulip Anton Trunov (Jan 13 2020 at 12:14):

by all means please do go ahead!

view this post on Zulip Karl Palmskog (Jan 13 2020 at 12:14):

I feel CFML is more of a framework personally, but could go either way

view this post on Zulip Karl Palmskog (Jan 13 2020 at 12:15):

I will probably add CoqEAL later today

view this post on Zulip Théo Zimmermann (Jan 13 2020 at 12:16):

OK the authors' description are clear:

view this post on Zulip Anton Trunov (Jan 13 2020 at 12:16):

btw, we are also missing Kami

view this post on Zulip Karl Palmskog (Jan 13 2020 at 12:18):

is Kami maintained? last commit was like 1 year ago

view this post on Zulip Anton Trunov (Jan 13 2020 at 12:18):

hmm, it feels like Kami is still a prominent Coq project

view this post on Zulip Anton Trunov (Jan 13 2020 at 12:19):

but I don’t have a strong opinion about that

view this post on Zulip Karl Palmskog (Jan 13 2020 at 12:19):

maybe we can check with Jason Gross, he has two open unmerged PRs

view this post on Zulip Karl Palmskog (Jan 13 2020 at 12:19):

I'm personally a bit averse to listing completely abandoned projects

view this post on Zulip Anton Trunov (Jan 13 2020 at 12:36):

How about these DeepSpec projects and their respective categories?

view this post on Zulip Karl Palmskog (Jan 13 2020 at 12:39):

CertiCoq has not seen complete release to my knowledge

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jan 13 2020 at 12:41):

hs-to-coq is fine

view this post on Zulip 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?

view this post on Zulip Anton Trunov (Jan 13 2020 at 12:43):

hs-to-coq it is then :) thanks

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 13 2020 at 12:51):

ah, and Metalib

view this post on Zulip Karl Palmskog (Jan 13 2020 at 12:52):

both have been used in multiple papers and so on

view this post on Zulip Anton Trunov (Jan 13 2020 at 12:59):

Isn’t Metalib stuck on Coq 8.6?

view this post on Zulip Karl Palmskog (Jan 13 2020 at 13:02):

nope

view this post on Zulip Karl Palmskog (Jan 13 2020 at 13:03):

I used it recently from GitHub

view this post on Zulip Karl Palmskog (Jan 13 2020 at 13:03):

in 8.10

view this post on Zulip Anton Trunov (Jan 13 2020 at 13:03):

:+1:

view this post on Zulip Anton Trunov (Jan 13 2020 at 13:08):

@Karl Palmskog Are we using the alphabetical order in Tools section?

view this post on Zulip Karl Palmskog (Jan 13 2020 at 13:08):

that's the intention, feel free to fix Menhir

view this post on Zulip Anton Trunov (Jan 13 2020 at 13:09):

ok

view this post on Zulip Karl Palmskog (Jan 13 2020 at 13:09):

some more candidates, Hahn, Coq-prelude, coq-haskell

view this post on Zulip Anton Trunov (Jan 13 2020 at 13:13):

Tested hs-to-coq on Coq 8.10 and added it to the list

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 13 2020 at 14:00):

I think they submitted stuff quite recently

view this post on Zulip Karl Palmskog (Jan 13 2020 at 14:00):

to the OPAM archive

view this post on Zulip Anton Trunov (Jan 13 2020 at 14:00):

oh, cool, hadn’t noticed that

view this post on Zulip Anton Trunov (Jan 13 2020 at 14:01):

ok, let us add it then

view this post on Zulip Anton Trunov (Jan 13 2020 at 14:02):

not sure about the section, though

view this post on Zulip Anton Trunov (Jan 13 2020 at 14:03):

maybe “tools"?

view this post on Zulip Anton Trunov (Jan 13 2020 at 14:05):

or, since they have a verified interpreter, it can go to the “Verified Software” section

view this post on Zulip Karl Palmskog (Jan 13 2020 at 14:06):

it's more verified software to me

view this post on Zulip Karl Palmskog (Jan 13 2020 at 14:06):

there might be a PL section at some point

view this post on Zulip Anton Trunov (Jan 13 2020 at 14:07):

yep, looks like we will need a more fine-grained categorization

view this post on Zulip 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

view this post on Zulip Anton Trunov (Jan 13 2020 at 14:27):

Perhaps we could re-categorize some of those by their purpose?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 13 2020 at 14:31):

I tried to follow the lead from OCaml and other awesome lists

view this post on Zulip Anton Trunov (Jan 13 2020 at 14:33):

e.g. awesome-ocaml list categorizes things by “areas”: Systems programming, Testing, Concurrency, etc.

view this post on Zulip Anton Trunov (Jan 13 2020 at 14:38):

speaking of SMT-Coq, I’m gonna add it if you don’t mind

view this post on Zulip 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

view this post on Zulip Anton Trunov (Jan 13 2020 at 14:38):

sure, np

view this post on Zulip Karl Palmskog (Jan 13 2020 at 15:14):

we should also add Mike Nahas' tutorial, which is apparently hosted in Coq's own repo

view this post on Zulip 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

view this post on Zulip Anton Trunov (Jan 13 2020 at 15:16):

:+1:

view this post on Zulip Théo Zimmermann (Jan 13 2020 at 15:45):

Mike Nahas' best location to reference is https://mdnahas.github.io/doc/nahas_tutorial.html

view this post on Zulip 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.

view this post on Zulip 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/

view this post on Zulip Karl Palmskog (Jan 13 2020 at 15:47):

OK good to know

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jan 13 2020 at 18:15):

hmm, this is interesting, it seems SiFive has rewritten Kami: https://github.com/sifive/Kami

view this post on Zulip Anton Trunov (Jan 13 2020 at 19:35):

yep, also noticed it, looks like we should add it

view this post on Zulip 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"

view this post on Zulip Karl Palmskog (Jan 25 2020 at 15:56):

w.r.t. this: https://twitter.com/CoqLang

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2020 at 15:57):

the official denomination is "The Coq Proof Assistant"

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2020 at 15:57):

and we often use Interactive Proof Assistant

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 25 2020 at 16:01):

so I would argue for one of the first two, just "Coq proof assistant" is fine...

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2020 at 16:03):

ok done!

view this post on Zulip Karl Palmskog (Jan 25 2020 at 16:04):

"interactive proof assistant" is mentioned twice on the Coq website

view this post on Zulip Karl Palmskog (Jan 25 2020 at 16:05):

once in the manual, once for some old workshop

view this post on Zulip 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

view this post on Zulip Anton Trunov (Jan 26 2020 at 20:03):

@Emilio Jesús Gallego Arias Cool background picture!

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2020 at 22:59):

:)

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2020 at 22:59):

Théo any comments on the mail I sent on twitter? (@zimmi48)

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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"

view this post on Zulip 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!

view this post on Zulip 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" :)

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 27 2020 at 12:21):

otherwise one might get lots of questions about what is "interactive proof assistant" vs. "proof assistant"

view this post on Zulip Karl Palmskog (Jan 27 2020 at 12:21):

I know at least paper reviewers complain about these things a lot...

view this post on Zulip 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"

view this post on Zulip Théo Zimmermann (Jan 27 2020 at 15:28):

I agree with Karl on being consistent and on ITP and "proof assistant" being standard.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Anton Trunov (Jan 28 2020 at 18:58):

@Karl Palmskog Any idea who we should talk to?

view this post on Zulip Karl Palmskog (Jan 28 2020 at 18:59):

my guess is that they didn't want it recorded?

view this post on Zulip Anton Trunov (Jan 28 2020 at 18:59):

oh, I see. I guess too late now :))

view this post on Zulip Karl Palmskog (Jan 28 2020 at 19:00):

I guess so yeah, but at least wanted to point this out

view this post on Zulip Emilio Jesús Gallego Arias (Jan 28 2020 at 19:00):

Ouch I only checked the last and first one so I thought

view this post on Zulip Emilio Jesús Gallego Arias (Jan 28 2020 at 19:00):

it is complete

view this post on Zulip Emilio Jesús Gallego Arias (Jan 28 2020 at 19:00):

not a big deal tho, if one is missing

view this post on Zulip Karl Palmskog (Jan 28 2020 at 19:01):

unsound tweet :wink:

view this post on Zulip Anton Trunov (Jan 28 2020 at 19:01):

hahaha

view this post on Zulip Emilio Jesús Gallego Arias (Jan 28 2020 at 19:01):

XDDDD

view this post on Zulip Anton Trunov (Jan 28 2020 at 19:01):

the sound of an unsound tweet

view this post on Zulip Emilio Jesús Gallego Arias (Jan 28 2020 at 19:01):

twitter's logic is paraconsistent tho

view this post on Zulip Emilio Jesús Gallego Arias (Jan 28 2020 at 19:01):

so we are allowed to do that

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Anton Trunov (Jan 28 2020 at 19:03):

This should go into awesome-type-theory-jokes list

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Jan 28 2020 at 19:05):

if there's any justice (true judgement?) it will go viral

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 28 2020 at 19:06):

OK, as long as it's on the TODO list, I won't complain

view this post on Zulip Anton Trunov (Jan 28 2020 at 19:06):

Emilio commented that way after I suggested to tweet about that post :)

view this post on Zulip 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?

view this post on Zulip Anton Trunov (Feb 02 2020 at 21:34):

(Not sure if this is the right room to discuss this topic)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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/

view this post on Zulip 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)

view this post on Zulip Anton Trunov (Feb 03 2020 at 15:40):

@Karl Palmskog Thanks for sharing. Cool slides! Are there any lecture notes?

view this post on Zulip Karl Palmskog (Feb 03 2020 at 15:41):

basically we have lecture slides + exercises

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 03 2020 at 15:43):

his LaTeX sources: https://github.com/thtuerk/ITP-course

view this post on Zulip Anton Trunov (Feb 03 2020 at 15:44):

:+1: Nice! Thanks again

view this post on Zulip 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

view this post on Zulip 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/

view this post on Zulip Anton Trunov (Feb 05 2020 at 14:39):

I opened an issue about that and CC’ed you.

view this post on Zulip Anton Trunov (Feb 05 2020 at 14:39):

btw, should we close https://github.com/coq-community/manifesto/issues/55 ?

view this post on Zulip Karl Palmskog (Feb 05 2020 at 14:47):

done

view this post on Zulip Anton Trunov (Feb 05 2020 at 14:47):

thanks

view this post on Zulip 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

view this post on Zulip Anton Trunov (Feb 07 2020 at 18:18):

:+1:

view this post on Zulip 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.?

view this post on Zulip Karl Palmskog (Feb 07 2020 at 18:30):

would be nice for sure

view this post on Zulip Karl Palmskog (Feb 07 2020 at 18:31):

assuming they don't need a lot of maintenance...

view this post on Zulip Anton Trunov (Feb 07 2020 at 18:32):

Great! I guess I’ll move this as a manifesto issue

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 07 2020 at 21:33):

@Théo Zimmermann perhaps I can count you as co-maintainer of the templates repo?

view this post on Zulip Karl Palmskog (Feb 07 2020 at 21:33):

sadly I'm clueless about Nix stuff

view this post on Zulip Théo Zimmermann (Feb 08 2020 at 15:16):

@Karl Palmskog Yes, add me there!

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 10 2020 at 20:30):

I think I'll put the usual coq-community issue to make a point...

view this post on Zulip Karl Palmskog (Feb 10 2020 at 20:31):

unfortunately thre license is unknown, but can probably be figured out by contacting authors

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Théo Zimmermann (Feb 11 2020 at 16:26):

I think less than this given the age of most open PRs.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 11 2020 at 17:11):

exponentially distributed

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Feb 13 2020 at 14:57):

Sure!

view this post on Zulip Karl Palmskog (Feb 13 2020 at 14:57):

we should be more liberal with help-wanted I think

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Feb 13 2020 at 14:58):

But we could extend this to something across more repos.

view this post on Zulip Théo Zimmermann (Feb 13 2020 at 14:58):

This works: https://github.com/issues?utf8=%E2%9C%93&q=is%3Aopen+is%3Aissue+archived%3Afalse+user%3Acoq-community+user%3Acoq+label%3A%22help+wanted%22+

view this post on Zulip Karl Palmskog (Feb 13 2020 at 14:58):

ah, maybe one can just modify the query a bit

view this post on Zulip Théo Zimmermann (Feb 13 2020 at 14:58):

user:coq-community + user:coq

view this post on Zulip Karl Palmskog (Feb 13 2020 at 14:58):

nice

view this post on Zulip Théo Zimmermann (Feb 13 2020 at 14:59):

"help wanted" might not be the right label though

view this post on Zulip Théo Zimmermann (Feb 13 2020 at 14:59):

as it does not imply low-effort

view this post on Zulip Karl Palmskog (Feb 13 2020 at 14:59):

right, but good-first-issue is not great either

view this post on Zulip Théo Zimmermann (Feb 13 2020 at 15:00):

well at least the meaning is clearer

view this post on Zulip Théo Zimmermann (Feb 13 2020 at 15:00):

and we can try to triage what's in there

view this post on Zulip Karl Palmskog (Feb 13 2020 at 15:01):

https://github.com/issues?utf8=%E2%9C%93&q=is%3Aopen+is%3Aissue+archived%3Afalse+user%3Acoq-community+user%3Acoq+label%3A%22good+first+issue%22+

view this post on Zulip Karl Palmskog (Feb 13 2020 at 15:02):

I guess this can be a good compromise, although some low-hanging fruit definitely requires expertise

view this post on Zulip 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+

view this post on Zulip Théo Zimmermann (Feb 13 2020 at 15:07):

sorted by :+1: https://github.com/issues?q=is%3Aopen+is%3Aissue+archived%3Afalse+user%3Acoq-community+user%3Acoq+user%3Amath-comp+label%3A%22good+first+issue%22+sort%3Areactions-%2B1-desc

view this post on Zulip Théo Zimmermann (Feb 13 2020 at 15:07):

Anyway, I'm not a big fan of this interface for showing these issues

view this post on Zulip Théo Zimmermann (Feb 13 2020 at 15:07):

Maybe we should look for an external service to help with this.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Feb 13 2020 at 15:09):

yeah

view this post on Zulip Anton Trunov (Feb 13 2020 at 16:40):

@Karl Palmskog Have you seen this https://github.com/awesomo4000/awesome-provable ?

view this post on Zulip 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

view this post on Zulip Anton Trunov (Feb 13 2020 at 16:43):

yeah, it’s not a competitor :)

view this post on Zulip Karl Palmskog (Feb 13 2020 at 16:43):

the good thing about focusing on Coq is that it fit in the PL category

view this post on Zulip Anton Trunov (Feb 13 2020 at 16:44):

Maybe we could mutually link?

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 13 2020 at 16:45):

yeah if we accumulate a few other lists we can create a section

view this post on Zulip Karl Palmskog (Feb 13 2020 at 16:45):

you could open an issue

view this post on Zulip Anton Trunov (Feb 13 2020 at 16:45):

cool!

view this post on Zulip Anton Trunov (Feb 13 2020 at 16:45):

I’m on it :)

view this post on Zulip Karl Palmskog (Feb 13 2020 at 16:45):

we can challenge the Lean people perhaps

view this post on Zulip Anton Trunov (Feb 13 2020 at 16:46):

:+1:

view this post on Zulip Karl Palmskog (Feb 13 2020 at 16:46):

to be clear, first step is probably an issue in awesome-coq

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 13 2020 at 16:47):

BitBucket dropping Mercurial sets a pretty bad precedent indeed...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 13 2020 at 18:23):

maybe we can ask him who is handling it

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Feb 13 2020 at 18:25):

Sorry I had missed half of your message

view this post on Zulip Anton Trunov (Feb 13 2020 at 20:25):

Any particular format of the presense of coq-community?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 14 2020 at 11:08):

Well, it was a joint idea with Bas Spitters, I imagined something like the following:

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Feb 14 2020 at 11:23):

Sounds good!

view this post on Zulip Anton Trunov (Feb 14 2020 at 11:34):

:+1:

view this post on Zulip 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)

view this post on Zulip Anton Trunov (Feb 14 2020 at 11:36):

LGTM!

view this post on Zulip Karl Palmskog (Feb 14 2020 at 11:36):

"platform - ecosystem - community" is a nice 'tripod' to stand on

view this post on Zulip Karl Palmskog (Feb 14 2020 at 15:41):

@Anton Trunov I did some quick investigation of the problems with porting CertiCrypt

view this post on Zulip Karl Palmskog (Feb 14 2020 at 15:41):

using the ALEA port

view this post on Zulip Karl Palmskog (Feb 14 2020 at 15:41):

there were some really strange mismatches between Set and Type

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Feb 16 2020 at 00:34):

The problem is also that Pierre Yves Strub said he would port it

view this post on Zulip Karl Palmskog (Feb 16 2020 at 00:35):

I didn't port much, just figured out one basic problem I can describe

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 17 2020 at 09:54):

https://github.com/EasyCrypt/certicrypt/blob/master/Semantics/Dlist.v#L164

view this post on Zulip Karl Palmskog (Feb 17 2020 at 09:55):

https://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html#DecidableSet

view this post on Zulip 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...

view this post on Zulip 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...

view this post on Zulip Anton Trunov (Feb 17 2020 at 10:43):

Could we use DecidableEq instead of DecidableEqSet ?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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).


view this post on Zulip Anton Trunov (Feb 17 2020 at 11:43):

afaikt

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 19 2020 at 15:24):

it turned out to be possible to fix the DepSet stuff and so on

view this post on Zulip Karl Palmskog (Feb 19 2020 at 15:27):

let me know and I can make the diff available...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 ?

view this post on Zulip Anton Trunov (Feb 19 2020 at 16:19):

@Emilio Jesús Gallego Arias Here it is https://github.com/coq-community/manifesto/issues/56

view this post on Zulip Anton Trunov (Feb 19 2020 at 16:19):

CertiCrypt, because of ALEA

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 19 2020 at 16:22):

for proof engineering research reasons alone, it's valuable

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 19 2020 at 17:12):

:thumbsup:

view this post on Zulip 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?

view this post on Zulip Anton Trunov (Feb 19 2020 at 17:35):

Yep, that’s the plan

view this post on Zulip 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

view this post on Zulip Pierre-Yves Strub (Feb 20 2020 at 10:00):

No answer from me because I’m on vacation

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Pierre-Yves Strub (Feb 20 2020 at 10:07):

I do not plan to maintain CertiCrypt alone.

view this post on Zulip Pierre-Yves Strub (Feb 20 2020 at 10:07):

I offered my help to port CertiCrypt to Coq 8.11.

view this post on Zulip Pierre-Yves Strub (Feb 20 2020 at 10:08):

I would be happy if Vladimir can help.

view this post on Zulip 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).

view this post on Zulip 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 :)

view this post on Zulip Pierre-Yves Strub (Feb 20 2020 at 10:16):

Anyway, maybe should we have a quick chat for organizing ourselves on the CertiCrypt side.

view this post on Zulip Pierre-Yves Strub (Feb 20 2020 at 10:16):

EOF (going back on vacation)

view this post on Zulip Karl Palmskog (Feb 20 2020 at 10:30):

:thumbsup: (all that sounds good to me)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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?]

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 20 2020 at 16:58):

something like research-artifact may be better

view this post on Zulip Théo Zimmermann (Feb 20 2020 at 16:59):

:+1:

view this post on Zulip Théo Zimmermann (Feb 20 2020 at 16:59):

Or even research-prototype if we want to insist on the non user-ready status.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 20 2020 at 17:02):

I don't mind advertising this more clearly

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Feb 20 2020 at 17:06):

:thumbsup: - will have the :tada: ready

view this post on Zulip 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...

view this post on Zulip Théo Zimmermann (Feb 20 2020 at 17:07):

Sure, that's life.

view this post on Zulip Karl Palmskog (Feb 20 2020 at 17:07):

I'm leaning towards docker-coq

view this post on Zulip Karl Palmskog (Feb 20 2020 at 17:08):

very important, but very specialized

view this post on Zulip Théo Zimmermann (Feb 20 2020 at 17:08):

What about Corn? More diversity.

view this post on Zulip Karl Palmskog (Feb 20 2020 at 17:09):

OK sounds good

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Anton Trunov (Feb 20 2020 at 19:31):

:+1:

view this post on Zulip 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! ]

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 24 2020 at 20:28):

if there needs to be URLs there, I recommend having them in full

view this post on Zulip Anton Trunov (Feb 25 2020 at 12:24):

@Karl Palmskog thanks, I missed that during review

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Anton Trunov (Feb 25 2020 at 15:39):

yep, I just discovered the same thing :)

view this post on Zulip Karl Palmskog (Feb 25 2020 at 15:40):

(2.0 and 3.0 are the only relevant versions of plain GPL)

view this post on Zulip Anton Trunov (Feb 25 2020 at 15:40):

@Karl Palmskog do you have the link where it says the license is LGPL?

view this post on Zulip Karl Palmskog (Feb 25 2020 at 15:44):

LICENSE file in coq-contribs repo

view this post on Zulip Anton Trunov (Feb 25 2020 at 15:47):

Thanks. Should it be LGPL-2.1-only or LGPL-2.1-or-later?

view this post on Zulip 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'

view this post on Zulip Anton Trunov (Feb 25 2020 at 15:49):

got it, thanks again

view this post on Zulip Gregory Malecha (Mar 04 2020 at 21:40):

does anyone know where coq's implementation of discrimintion trees is and how deep they go?

view this post on Zulip Karl Palmskog (Mar 11 2020 at 19:18):

@Théo Zimmermann sorry to pile on, but is the domain thing still on your agenda?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Mar 11 2020 at 19:27):

Yes, if you can create this repo, that would be great.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Mar 11 2020 at 19:52):

Yes, I'm always doing this for my own website.

view this post on Zulip 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

view this post on Zulip Maxime Dénès (Mar 12 2020 at 08:27):

and I'd bet they are more aware than team assistants for this matter

view this post on Zulip Maxime Dénès (Mar 12 2020 at 08:27):

We can talk a bit this afternoon about it if you like.

view this post on Zulip 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?

view this post on Zulip Maxime Dénès (Mar 12 2020 at 14:21):

now is fine

view this post on Zulip Karl Palmskog (Mar 12 2020 at 15:43):

@Théo Zimmermann was there any conclusion on the domain issue?

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Mar 12 2020 at 16:32):

OK

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Mar 13 2020 at 11:38):

@Théo Zimmermann OK, I will put something there later this afternoon

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Gregory Malecha (Mar 13 2020 at 20:56):

is it best to ask on /coq

view this post on Zulip Karl Palmskog (Mar 13 2020 at 20:56):

yes, either there or in the Discourse forum

view this post on Zulip Gregory Malecha (Mar 13 2020 at 20:56):

ok, thanks

view this post on Zulip Karl Palmskog (Mar 13 2020 at 20:57):

if you think the answer is of general value, I recommend the Discourse

view this post on Zulip Karl Palmskog (Mar 13 2020 at 20:57):

much more searchable etc.

view this post on Zulip Gregory Malecha (Mar 13 2020 at 20:57):

thanks

view this post on Zulip 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

view this post on Zulip 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;"

view this post on Zulip 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 !

view this post on Zulip Bas Spitters (Mar 14 2020 at 09:09):

Is there any order in the "current projects" ?

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Mar 14 2020 at 12:44):

I can change the initial stuff on hosting and add something about applications you mentioned

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Mar 14 2020 at 17:36):

that should make a project list a lot easier to navigate

view this post on Zulip 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

view this post on Zulip Bas Spitters (Mar 15 2020 at 21:15):

@Karl Palmskog Seems reasonable enough. Thanks!

view this post on Zulip Karl Palmskog (Mar 15 2020 at 21:18):

ideally we would store categorization metadata in each project and extract it dynamically

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Mar 17 2020 at 08:34):

@Théo Zimmermann so what do you think of the categorization? https://coq-community.github.io

view this post on Zulip 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)

view this post on Zulip Théo Zimmermann (Mar 17 2020 at 14:50):

@Karl Palmskog OK, now in the queue.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Mar 17 2020 at 14:51):

yes, just generated via pandoc: pandoc -s -o index.html index.md, feel free to update

view this post on Zulip Théo Zimmermann (Mar 17 2020 at 14:51):

OK

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Mar 17 2020 at 14:53):

:+1:

view this post on Zulip Théo Zimmermann (Mar 17 2020 at 14:54):

Unfortunately, regenerating the HTML using the same command changes a bunch of unrelated stuff :S

view this post on Zulip Karl Palmskog (Mar 17 2020 at 14:54):

we may have different versions of pandoc

view this post on Zulip Karl Palmskog (Mar 17 2020 at 14:55):

but doesn't matter if the content is the same

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Mar 17 2020 at 15:02):

And possibly link to the contributing guide.

view this post on Zulip Théo Zimmermann (Mar 17 2020 at 15:03):

But very good job, thanks!

view this post on Zulip Théo Zimmermann (Mar 17 2020 at 15:07):

Coqoban does probably better fit the Documentation and Tutorials category.

view this post on Zulip Karl Palmskog (Mar 17 2020 at 15:07):

in some sense, but also, it's a "verified puzzle"

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Mar 17 2020 at 15:08):

For instance with a :star: and a :warning:

view this post on Zulip Karl Palmskog (Mar 17 2020 at 15:08):

I would say "experimental" rather than "low quality"

view this post on Zulip Théo Zimmermann (Mar 17 2020 at 15:08):

Sure

view this post on Zulip Théo Zimmermann (Mar 17 2020 at 15:08):

or WIP

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Mar 17 2020 at 15:09):

yeah good point

view this post on Zulip Karl Palmskog (Mar 17 2020 at 15:10):

but how do you think we should store categories and labels? meta.yml?

view this post on Zulip Théo Zimmermann (Mar 17 2020 at 15:20):

possibly yes

view this post on Zulip 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).

view this post on Zulip Karl Palmskog (Mar 17 2020 at 15:21):

sounds good

view this post on Zulip Karl Palmskog (Mar 17 2020 at 15:22):

I'll keep the :tada:s ready

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Mar 17 2020 at 15:24):

and maybe our README.md template should include a link to the Coq website somewhere

view this post on Zulip Théo Zimmermann (Mar 17 2020 at 15:24):

interesting thought indeed!

view this post on Zulip Karl Palmskog (Mar 17 2020 at 15:24):

all for marketing reasons and so on

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Mar 18 2020 at 16:01):

I see, I guess we'll just wait and see then

view this post on Zulip Karl Palmskog (Mar 20 2020 at 12:13):

http://coq-community.org is up! :tada:

view this post on Zulip 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)

view this post on Zulip Karl Palmskog (Mar 20 2020 at 12:28):

now it works, that was fast: https://coq-community.org/

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Mar 20 2020 at 13:01):

well, not only the website works, but also project websites like: https://coq-community.org/reglang

view this post on Zulip Guillaume Claret (Gitter import) (Mar 20 2020 at 13:01):

:tada:

view this post on Zulip Théo Zimmermann (Mar 20 2020 at 13:02):

:rocket:

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Mar 20 2020 at 13:02):

those look good to me

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Mar 20 2020 at 13:05):

warnings based on READMEs: ParamCoq, Exact real arithmetic, bits

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Mar 20 2020 at 13:09):

(Not sure @Maxime Dénès would disagree)

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Mar 20 2020 at 13:10):

well, it was based on that people reported it usable

view this post on Zulip Karl Palmskog (Mar 20 2020 at 13:10):

and VSCode support is a hot topic, etc.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Mar 20 2020 at 13:13):

that's probably true, yes

view this post on Zulip Paolo Giarrusso (Mar 20 2020 at 13:20):

I have recommended vscoq to colleagues, but the experience includes Coq crashing, interruption failing, etc.

view this post on Zulip Paolo Giarrusso (Mar 20 2020 at 13:21):

But if you come in expecting a finished product, you’ll be very disappointed, I think.

view this post on Zulip Théo Zimmermann (Mar 20 2020 at 13:21):

So indeed, that sounds to early to give it a :star:

view this post on Zulip Théo Zimmermann (Mar 20 2020 at 13:22):

Not having a :star: won't prevent people to use it BTW

view this post on Zulip Paolo Giarrusso (Mar 20 2020 at 13:22):

(Sorry, “coq crashing “ isn’t accurate, but you must restart the plugin often enough)

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Mar 21 2020 at 13:18):

You can just open issues in the bot bug tracker.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Mar 21 2020 at 16:56):

so nothing related to the OPAM index/archive unless it can be done with the bot?

view this post on Zulip Karl Palmskog (Mar 21 2020 at 16:58):

I would argue there is some low-hanging fruit there

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Apr 15 2020 at 14:12):

Yes, I agree.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Cyril Cohen (Apr 15 2020 at 18:17):

https://leanprover-community.github.io/archive/

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Apr 15 2020 at 18:53):

Interesting!

view this post on Zulip Dan Frumin (Gitter import) (Apr 16 2020 at 09:27):

So this chat will be moving to Zulip?

view this post on 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.)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gregory Malecha (May 03 2020 at 20:39):

does anyone know how to record dependency information in the meta.yml file from coq-templates?

view this post on Zulip Karl Palmskog (May 03 2020 at 21:02):

@Gregory Malecha sure, what you want to know?

view this post on Zulip 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

view this post on Zulip Gregory Malecha (May 03 2020 at 21:03):

e.g. my project depends on coq-ext-lib and coq-template-coq

view this post on Zulip 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)

view this post on Zulip Gregory Malecha (May 03 2020 at 21:03):

also iris and stdpp

view this post on Zulip Karl Palmskog (May 03 2020 at 21:04):

basically, it's a list, so each dependency has to start with -

view this post on Zulip Karl Palmskog (May 03 2020 at 21:04):

@Gregory Malecha so which versions of coq-ext-lib and coq-template-coq?

view this post on Zulip Gregory Malecha (May 03 2020 at 21:04):

i see

view this post on Zulip Gregory Malecha (May 03 2020 at 21:04):

ok, great

view this post on Zulip Karl Palmskog (May 03 2020 at 21:05):

I can vet the meta.yml for you if you write something

view this post on Zulip Gregory Malecha (May 03 2020 at 21:05):

that would be great

view this post on Zulip 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

view this post on Zulip Gregory Malecha (May 03 2020 at 21:06):

which is obviously not an ocaml dependency

view this post on Zulip Karl Palmskog (May 03 2020 at 21:06):

that can be added as an OPAM dependency

view this post on Zulip Gregory Malecha (May 03 2020 at 21:06):

how?

view this post on Zulip Karl Palmskog (May 03 2020 at 21:07):

usually "conf-clang" {build}

view this post on Zulip Karl Palmskog (May 03 2020 at 21:07):

if it's only in the build phase

view this post on Zulip 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

view this post on Zulip Gregory Malecha (May 03 2020 at 21:07):

ah

view this post on Zulip Gregory Malecha (May 03 2020 at 21:07):

ok

view this post on Zulip Gregory Malecha (May 03 2020 at 21:08):

the project contains two pieces, a coq formalization and a tool built on clang

view this post on Zulip Gregory Malecha (May 03 2020 at 21:08):

so clang is needed in "all" phases

view this post on Zulip Karl Palmskog (May 03 2020 at 21:08):

well, you can just omit {build}

view this post on Zulip Gregory Malecha (May 03 2020 at 21:08):

ok

view this post on Zulip Gregory Malecha (May 03 2020 at 21:09):

that is great

view this post on Zulip Karl Palmskog (May 03 2020 at 21:09):

note that there is also conf-g++

view this post on Zulip 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

view this post on Zulip Gregory Malecha (May 03 2020 at 21:10):

i see

view this post on Zulip Gregory Malecha (May 03 2020 at 21:10):

thanks

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Gregory Malecha (May 03 2020 at 21:12):

so they just clone out of the same repo but have different build targets?

view this post on Zulip Karl Palmskog (May 03 2020 at 21:12):

right

view this post on Zulip Gregory Malecha (May 03 2020 at 21:12):

is there a standard naming convention for that

view this post on Zulip Karl Palmskog (May 03 2020 at 21:12):

not really

view this post on Zulip Gregory Malecha (May 03 2020 at 21:12):

the whole project is called cpp2v

view this post on Zulip Gregory Malecha (May 03 2020 at 21:13):

coq-cpp2v and coq-cpp2v-bin

view this post on Zulip Karl Palmskog (May 03 2020 at 21:13):

I can show you how we did it in CoqHammer

view this post on Zulip Gregory Malecha (May 03 2020 at 21:13):

or something liekthat

view this post on Zulip Gregory Malecha (May 03 2020 at 21:13):

that would be great

view this post on Zulip 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}
]

view this post on Zulip Karl Palmskog (May 03 2020 at 21:14):

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~"}
]

view this post on Zulip Gregory Malecha (May 03 2020 at 21:14):

i see

view this post on Zulip Gregory Malecha (May 03 2020 at 21:15):

great

view this post on Zulip Karl Palmskog (May 03 2020 at 21:15):

ah, I assume this is related to a certain recent submission?

view this post on Zulip Gregory Malecha (May 03 2020 at 21:15):

yes

view this post on Zulip Gregory Malecha (May 03 2020 at 21:16):

:-)

view this post on Zulip 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)

view this post on Zulip Karl Palmskog (May 03 2020 at 21:21):

that is, if one has two local OPAM package definitions

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (May 03 2020 at 21:28):

no, it can be done

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (May 03 2020 at 21:49):

opam doesn't really allow you to say in which repository a package is defined

view this post on Zulip 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

view this post on Zulip Gregory Malecha (May 03 2020 at 21:50):

so i just list the dependency as usual and then document the opam repo add command?

view this post on Zulip Gregory Malecha (May 03 2020 at 21:50):

that makes sense

view this post on Zulip Karl Palmskog (May 03 2020 at 21:50):

right

view this post on Zulip Gregory Malecha (May 03 2020 at 21:50):

thanks for your help

view this post on Zulip Karl Palmskog (May 03 2020 at 21:50):

np

view this post on Zulip 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

view this post on Zulip Gregory Malecha (May 03 2020 at 21:53):

i'm not familiar with how dev packages work

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Gregory Malecha (May 03 2020 at 21:56):

i see

view this post on Zulip Gregory Malecha (May 03 2020 at 21:56):

thanks

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Gregory Malecha (May 05 2020 at 19:19):

it is actualy copying my projects "description" over and over again

view this post on Zulip Théo Zimmermann (May 05 2020 at 20:05):

it would be easier to understand with a link to some code

view this post on Zulip Gregory Malecha (May 05 2020 at 20:14):

https://gist.github.com/gmalecha/4eb22d2267c502ff8bfd0fb4d4eef13f

view this post on Zulip Gregory Malecha (May 05 2020 at 20:15):

when i run that through mustache

view this post on Zulip Gregory Malecha (May 05 2020 at 20:15):

i get

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (May 05 2020 at 20:18):

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.

view this post on Zulip Gregory Malecha (May 05 2020 at 20:19):

ah, thanks

view this post on Zulip Théo Zimmermann (May 05 2020 at 20:19):

We could avoid this by renaming the description within the dependency field into something else.

view this post on Zulip Théo Zimmermann (May 05 2020 at 20:19):

Let me try something

view this post on Zulip Théo Zimmermann (May 05 2020 at 20:29):

See https://github.com/coq-community/templates/pull/27


Last updated: Feb 05 2023 at 15:03 UTC