Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • 18:37
    JasonGross commented #3988
  • 18:35
    rnrand opened #10687
  • 18:25
    ejgallego commented #10686
  • 18:15
    ejgallego commented #10686
  • 18:08
    ejgallego commented #10647
  • 17:59
    sliverdragon37 starred coq/coq
  • 17:49
    Zimmi48 edited #10686
  • 17:47
    Zimmi48 review_requested #10686
  • 17:47
    Zimmi48 labeled #10686
  • 17:47
    Zimmi48 opened #10686
  • 17:31
  • 16:27
    ejgallego commented #10515
  • 16:25
    Zimmi48 closed #10515
  • 16:24

    Zimmi48 on master

    [dune] Move to Dune 1.10, use c… Merge PR #10515: [dune] Move to… (compare)

  • 16:24
    Zimmi48 commented #10515
  • 15:23

    vbgl on v8.10

    Remove links to doc artifacts a… Backport PR #10671: Remove link… Std++, Iris, and Lambda-Rust ha… and 1 more (compare)

  • 15:13
    vbgl synchronize #9963
  • 15:13
    mattam82 commented #9062
  • 15:10
    vbgl commented #9062
  • 15:05
    ejgallego commented #9062
Pierre-Marie Pédrot
@ppedrot
if you evaluate this as a whole, force all thunks and reevaluate the last line, then the constraints are not here
Gaëtan Gilbert
@SkySkimmer
yeah when you backtrack the universe checking is undone
Pierre-Marie Pédrot
@ppedrot
supâ goreito
anyways, not a really serious unsoundness
probably closer to a Pollack inconsistency
Gaëtan Gilbert
@SkySkimmer
I guess in the global env unfreeze_function we could go through the delayed universes and add the ones which are ready to the graph
might be costly though
Pierre-Marie Pédrot
@ppedrot
dunno
state + parallelism + backtracking is hard
without a proper semantic model we're bound to write flaky code
Karl Palmskog
@palmskog
it seems the opam archive CI issue goes deeper, now even Coq 8.5.0 (as opposed to just dev) won't install in 4.05.0 jobs
Valentin Robert
@Ptival
why does the positive scope not seem to work in 8.9?
From Coq Require Import Numbers.BinNums.
Definition one : positive := 1%positive.
Karl Palmskog
@palmskog
this is really great stuff, many packages here that do not have regular releases: https://coq-bench.github.io/clean/Linux-x86_64-4.02.3-2.0.1/extra-dev/
Théo Zimmermann
@Zimmi48

@Ptival

  • Syntax notations for string, ascii, Z, positive, N, R, and int31 are no longer available merely by Requireing the files that define the inductives. You must Import Coq.Strings.String.StringSyntax (after Require Coq.Strings.String), Coq.Strings.Ascii.AsciiSyntax (after Require Coq.Strings.Ascii), Coq.ZArith.BinIntDef, Coq.PArith.BinPosDef, Coq.NArith.BinNatDef, Coq.Reals.Rdefinitions, and Coq.Numbers.Cyclic.Int31.Int31, respectively, to be able to use these notations. Note that passing -compat 8.8 or issuing Require Import Coq.Compat.Coq88 will make these notations available. Users wishing to port their developments automatically may download fix.py from https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169 and run a command like while true; do make -Okj 2>&1 | /path/to/fix.py; done and get a cup of coffee. (This command must be manually interrupted once the build finishes all the way though. Note also that this method is not fail-proof; you may have to adjust some scopes if you were relying on string notations not being available even when string_scope was open.)

(extract from the changelog)

Valentin Robert
@Ptival
aaaah, thanks!
Talia Ringer
@tlringer
I ended up defining a state monad and writing a bunch of HOFs using that for evar_maps in my code. I don't know if they are all correct yet, though. DEVOID seems to be doing nicely with these, but PUMPKIN PATCH isn't ported yet so some of them might be wrong. https://github.com/uwplse/coq-plugin-lib/blob/master/src/coq/logicutils/contexts/stateutils.ml
idk if you guys already have something like this. presumably at some point I'll be using EConstr in more places, but it looks like a lot of the Coq API uses constr, so it doesn't seem like an easy port (i got kind of stuck trying to do it in a different branch yesterday)
Gaëtan Gilbert
@SkySkimmer
note that https://github.com/coq/coq/blob/master/clib/monad.mli Monad.Make defines a few of the list combinators
Karl Palmskog
@palmskog
these packages/projects that have flaky builds (likely due to nondeterminism in make parallel jobs) is something keep an eye on, probably they should either switch to dune or always use a single make job: https://github.com/coq-bench/make-html/blob/master/black_list.rb
Gaëtan Gilbert
@SkySkimmer
are any of those the current version
?
Guillaume Claret
@clarus
coq-coq2html and coq-plugin-utils.1.3.0 are in the latest version for example
Maxime Dénès
@maximedenes
guys, did we schedule a working group? @mattam82
Gaëtan Gilbert
@SkySkimmer

the wiki is authoritative

The next Coq Working Group will (tentatively) happen in the early fall 2019.

Karl Palmskog
@palmskog
authoritatively vague, when will the date be set? (would 100% like to join in for the OPAM topic)
Gaëtan Gilbert
@SkySkimmer
looks like github has started sending email notifications for force pushes
if only it had happened before @MSoegtropIMC had his issue (cf coqdev) :v
Théo Zimmermann
@Zimmi48
The timeline is also supposed to show the force-push history now though.
@palmskog Are you suggesting to make the WG happen on the week when you will be in Paris?
Karl Palmskog
@palmskog
@Zimmi48 would be convenient, but obviously convenience for me shouldn't be a decider, I can join remotely
Matthieu Sozeau
@mattam82
Nope, not scheduled yet, will send a doodle today for end of September. We were suggesting maybe having it in Nantes, I’ll put the option there as well
Vincent Laporte
@vbgl
Hi. Does anyone know why the double-negation-elimination lemma is called NNPP?
Matthieu Sozeau
@mattam82
Not-not-P-implies-P
Vincent Laporte
@vbgl
Interesting. Thanks.
Maxime Dénès
@maximedenes
@mattam82 unfortunately, Nantes is going to be too inconvenient for us (from Nice)
we just checked the flights, there's only one per day at an inconvenient time
it would mean three days of stay/travel for one day of meeting
pity
Matthieu Sozeau
@mattam82
Ah. When are the flights?
Maxime Dénès
@maximedenes
middle of the day
Matthieu Sozeau
@mattam82
Oh I forgot to say we’ll do two days
Zut
Ok. We could start at middday and end at midday with two nights to accommodate this.
Maxime Dénès
@maximedenes
not easy
the flight to Nantes lands at 2pm
and the return takes off at 10am...
so with two nights, we can basically work one day and two hours
not worth it
Matthieu Sozeau
@mattam82
Indeed, that's not ideal
Gaëtan Gilbert
@SkySkimmer
is azure windows having issues recently?
Jason Gross
@JasonGross
coq/coq#1433 is assigned to @barras and has no comments since 2016. Should I (we) unassign him? (Also, is there any hope of getting a dev to implement this extension to the positivity checker, which was requested in 2002?)
Gaëtan Gilbert
@SkySkimmer
old issue assignments, especially those automatically ported from bugzilla, should be removed as they reflect no reality