imported from gitter room coq/Equations · Equations devs & users

It's been a while since we discussed replacing the backend of Function by Equations, did you make some advances?

Matthieu Sozeau (Jan 25 2018 at 04:46):

Not exactly, it’s clearer what is missing now: the factorization of cases and a way to interpret concrete syntax to splitting trees, Thierry Martinez is working on that.

Pierre Courtieu (Jan 25 2018 at 11:06):

Jad Hamza (Gitter import) (Apr 06 2018 at 11:34):

On paper it would be like proving by induction on n that there exists such a function f, and that f n = match [...]. (We strengthen the induction hypothesis by adding the equality as part of the goal). Then, as long as we use that induction hypothesis on strictly smaller arguments then it seems it should be sound?

Jad Hamza (Gitter import) (Apr 06 2018 at 11:39):

@Matthieu Sozeau Since you're there :) Do you have an explanation as to why this id (x :: l) doesn't reduce to x :: id l (https://gist.github.com/jad-hamza/ff6b07794856cfdd04e1fe94d4673688) when using Program Fixpoint? With Equations it works fine thanks to the rewrite lemmas

Jad Hamza (Gitter import) (Apr 09 2018 at 11:45):

Hello, is it possible to change the tactic used by Equations? I have a tactic set with Obligation Tactic, but Equations doesn't seem to be using it. Then when I do "Next Obligation", the tactic is indeed used and the goal is solved.

Matthieu Sozeau (Apr 12 2018 at 09:00):

Jad Hamza (Gitter import) (Apr 12 2018 at 11:01):

@Matthieu Sozeau Alright thanks, I'll try to make a small example to report an issue if I encounter the bug again

Jad Hamza (Gitter import) (Apr 13 2018 at 11:49):

Jad Hamza (Gitter import) (Apr 18 2018 at 18:09):

I'm trying "opam install coq-equations" with coq.8.8.0 but it's asking me to downgrade coq to 8.7.2 (I do have the repo: https://coq.inria.fr/opam/extra-dev)

Matthieu Sozeau (Apr 19 2018 at 16:39):

Jad Hamza (Gitter import) (Apr 25 2018 at 12:48):

Hello @Matthieu Sozeau, I'm using the Equations package 8.7.dev on Coq 8.7.2, and I'm having some trouble on "Qed" or "Admitted" on obligations. It's taking very long (5 minutes and running now). Is this a known issue?

Matthieu Sozeau (Apr 25 2018 at 12:57):

It can be failing to prove induction/elimination principles in presence of obligations. One way to avoid this is to abstract them as sublemmas before the definition. Not ideal but works well.

Matthieu Sozeau (Apr 25 2018 at 12:57):

Jad Hamza (Gitter import) (Apr 25 2018 at 13:11):

Aleksey Nogin (Gitter import) (Apr 26 2018 at 17:50):

Is there a way to define several (>2) mutually recursive functions? If so, what is the right syntax? As far as I can tell, I can only have one "where" (when I tried adding two, weirdness happened - I posted issue mattam82/Coq-Equations#74 about it).

Aleksey Nogin (Gitter import) (Apr 27 2018 at 14:21):

@Matthieu Sozeau, thanks a lot for looking into mattam82/Coq-Equations#74 - please do not hesitate to let me know if I can be of any help with narrowing this down, or testing a potential solution (for this or any of the other issues I am reporting).

Jad Hamza (Gitter import) (May 01 2018 at 05:18):

Aleksey Nogin (Gitter import) (May 01 2018 at 18:44):

@Matthieu Sozeau, since I reported so many issues, I thought it would be worth providing an update on which one(s) I care about the most - currently out development is blocked by inability to define equations involving VST's compact_prod (https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L6) - a combination of mattam82/Coq-Equations#78 and the bugs that crop up when trying to work around it (mattam82/Coq-Equations#84, mattam82/Coq-Equations#85, but not actually seeing mattam82/Coq-Equations#82 "in production").

Aleksey Nogin (Gitter import) (May 01 2018 at 20:55):

Actually, I may have spoken too soon - while the mattam82/Coq-Equations#78 is definitely and issue for us, if/when it is fixed, we might still end up struggling with mattam82/Coq-Equations#74 as well.

Aleksey Nogin (Gitter import) (May 02 2018 at 16:52):

For issues where things result in an unexpected typechecking error, is there a way to have everything generated by the plugin printed, so that we can see the context for the type error, and know where exactly it's occurring?

Matthieu Sozeau (May 03 2018 at 12:19):

Ok, I’ll try to have a look at those two in priority! Sadly my laptop broke two days ago so I’ve not been able to hack around as much as I’d like!

Aleksey Nogin (Gitter import) (May 03 2018 at 20:54):

Aleksey Nogin (Gitter import) (May 14 2018 at 16:49):

I came up with a potential workaround for mattam82/Coq-Equations#78 (posted it as a comment there), but when I tried to apply it in production, I got

Induction principle could not be proved automatically:
Anomaly "Helper not found while proving induction lemma."

I do not have a good way to reproduce it yet, but will see if I can create one.

Aleksey Nogin (Gitter import) (May 14 2018 at 17:52):

So far, all my attempts to reproduce the Anomaly error above in a simplified example hit either mattam82/Coq-Equations#84 or mattam82/Coq-Equations#85 instead...

Matthieu Sozeau (May 14 2018 at 18:04):

Matthieu Sozeau (May 14 2018 at 18:05):

If I fix the issue that struct does not work on a single definition we might make progress as well, no?

Aleksey Nogin (Gitter import) (May 14 2018 at 18:09):

No, I do not have anything blocking on "Equations (struct id)" not working - the workaround was to move some of the arguments into a return type. Currently, I am stuck on needing to define >2 mutually recursive functions (mattam82/Coq-Equations#74) and the Anomaly "Helper not found while proving induction lemma." issue.

Matthieu Sozeau (May 14 2018 at 18:10):

Ok, thanks for the update. Let's see if I can get the >2 mutuals first, its pretty well localised

Aleksey Nogin (Gitter import) (May 14 2018 at 18:17):

Thanks, I'll continue trying to get a reproducible case for the Anomaly in the meantime.

Matthieu Sozeau (May 14 2018 at 18:30):

I guess in your "production" case you additionally have nesting? That would explain the "helper not found" message

Aleksey Nogin (Gitter import) (May 14 2018 at 18:31):

Matthieu Sozeau (May 14 2018 at 18:31):

Aleksey Nogin (Gitter import) (May 14 2018 at 18:33):

Right, it has stuff along the lines of my examples in mattam82/Coq-Equations#84 / mattam82/Coq-Equations#85

Aleksey Nogin (Gitter import) (May 14 2018 at 19:30):

Was finally able to reproduce the Anomaly - filed mattam82/Coq-Equations#93 (see the P.S. comment there for what makes a difference between hitting mattam82/Coq-Equations#84 and getting past it).

Aleksey Nogin (Gitter import) (May 16 2018 at 15:54):

@Matthieu Sozeau: thanks a lot for the mattam82/Coq-Equations#74 fix! Any chance it could be backported to a stable branch (e.g, 8.8)?

Matthieu Sozeau (May 16 2018 at 16:16):

Matthieu Sozeau (May 16 2018 at 16:39):

Aleksey Nogin (Gitter import) (May 16 2018 at 16:39):

Jad Hamza (Gitter import) (May 17 2018 at 12:54):

Hi @Matthieu Sozeau, I have a quick question: how can I prevent automatic unfolding of a function defined by Equations?

Jad Hamza (Gitter import) (May 17 2018 at 13:17):

Jad Hamza (Gitter import) (May 17 2018 at 13:21):

I'm trying with Arguments f x y : simpl never. but cbn still unfolds it. On the other hand, cbn -[f] has the write behavior and does not unfold f.

Matthieu Sozeau (May 17 2018 at 13:24):

You can use Opaque / Transparent. The system should just be entirely parameterized with the current things one wants to unfold or not but currently only imperative state handling is available and reliable :)

Jad Hamza (Gitter import) (May 17 2018 at 13:27):

Matthieu Sozeau (May 17 2018 at 13:28):

Matthieu Sozeau (May 17 2018 at 13:29):

Maybe you can use a custom simplification tactic? There must be an issue on Coq’s github that adresses this, otherwise it would be good to submit one!

Jad Hamza (Gitter import) (May 17 2018 at 13:30):

@Matthieu Sozeau Yes I'll check! I'll use simpl for now. I have another quick question

Jad Hamza (Gitter import) (May 17 2018 at 13:31):

I now want to simplify the function call thanks the equations generated by Equations, so I do:

repeat rewrite f_equation_1 in * || rewrite f_equation_2 in * || rewrite f_equation_3 in * || rewrite f_equation_4 in * || rewrite f_equation_5 in *.

Jad Hamza (Gitter import) (May 17 2018 at 13:31):

Jad Hamza (Gitter import) (May 17 2018 at 13:35):

Jad Hamza (Gitter import) (May 17 2018 at 13:37):

@Matthieu Sozeau Oh, actually "constructor" also unfolds f to f_comp_proj when the goal is f x y

Matthieu Sozeau (May 17 2018 at 13:44):

Matthieu Sozeau (May 17 2018 at 13:45):

Jad Hamza (Gitter import) (May 17 2018 at 13:47):

wait, in fact cbn seems to respect Opaque, but not constructor. Thanks for simp. Also the slowness disappeared now after rebooting emacs, I don't know what happened, and the rewrite f_equation_i works as expected

Matthieu Sozeau (May 17 2018 at 14:39):

Matthieu Sozeau (May 18 2018 at 16:27):

@Aleksey Nogin I’m almost done fixing #93 and supporting definitions whose return type is a function type everywhere

Jad Hamza (Gitter import) (May 23 2018 at 10:21):

Matthieu Sozeau (May 23 2018 at 12:57):

I’ll try to have a look today. If you inspect the rewrite hint databases and the transparency status of constants do you see anything suspect maybe?

Jad Hamza (Gitter import) (May 23 2018 at 13:39):

@Matthieu Sozeau Thanks! Do you mean Print Rewrite HintDb core.? I just see rewrite rules about the composition of two functions.

Jad Hamza (Gitter import) (May 23 2018 at 13:42):

Print Transparent Dependencies transport. prints a bunch of dependencies but I guess these are the normal library dependencies?

Matthieu Sozeau (May 23 2018 at 13:45):

I mean Print Rewrite HintDb yes, is there a difference if the definitions are in one file and multiple ones ?

Matthieu Sozeau (May 23 2018 at 13:47):

About/Print cst. Should tell you if cst is transparent or opaque, that might drastically change the time of simp if the definitions are transparent

Jad Hamza (Gitter import) (May 23 2018 at 13:55):

@Matthieu Sozeau About transport tells me that transport is transparent when there are two files. When everything is in the same file, I get: transport is basically transparent but considered opaque for reduction

Jad Hamza (Gitter import) (May 23 2018 at 14:03):

When there are two files, Opaque transport. solves the slowness. Maybe I should just set all Equations definitions to Opaque?

Matthieu Sozeau (May 23 2018 at 15:46):

I’ve hit the problem a few times as well, I think this deserves an issue and a fix

Matthieu Sozeau (May 23 2018 at 15:47):

The fact that the Opaque flag is not exported properly is another one. I don’t know if I can do it from the plugin side, I’ll have to try

Aleksey Nogin (Gitter import) (May 23 2018 at 17:55):

Thanks! Looking forward to using it. (Note however that returning a function type, as opposed to just passing an argument directly, was only needed as a workaround to some of the other issues I was hitting)

Matthieu Sozeau (May 23 2018 at 18:01):

Yes I know, but it's a necessary step to treat properly definitions like [Eqns foo : a -> b -> c := foo x := ...] which were requested as well and it fixes the treatment of partial applications of recursive calls when building the graph and a few other things. My branch fix93auto works entirely now, but for spurious induction hypotheses in the graph in some dependent cases. I think I'll merge that first and try to improve cleaning later.

Aleksey Nogin (Gitter import) (May 23 2018 at 18:02):

Matthieu Sozeau (May 24 2018 at 12:12):

Aleksey Nogin (Gitter import) (May 29 2018 at 16:56):

@Matthieu Sozeau: Thanks a lot! I just filed two new issues, but not sure whether they are are something I care about - it could be that I am hitting them in my code because I have a placeholder case where I have not yet done the proper implementation - and it's that placeholder case that's triggering the issues, not something I'd actually care about. I will let you know what I find out once I replace the placeholder with the "real" implementation.

Matthieu Sozeau (May 29 2018 at 17:43):

Aleksey Nogin (Gitter import) (May 29 2018 at 22:48):

Aleksey Nogin (Gitter import) (May 29 2018 at 23:34):

I just reported mattam82/Coq-Equations#100 - this one I am actually blocked on... The error message is vague enough that I am not sure whether it's my fault or Equations', but even if it's mine, I do not see it...

Aleksey Nogin (Gitter import) (May 30 2018 at 14:21):

@Matthieu Sozeau, thanks a lot for pointing out where I was going wrong with mattam82/Coq-Equations#100. With my error fixed, I am now hitting mattam82/Coq-Equations#98 in a way that stumps me. Note that while in the simple example that I posted in mattam82/Coq-Equations#98, the error message shows up by itself, in my "production" implementation, it shows up in the middle of a long sequence of messages with things being successfully defined and obligations being successfully discharged...

Matthieu Sozeau (May 30 2018 at 17:20):

There’s something wrong in the inductive graph production, but I didn’t pinpoint where yet.

Matthieu Sozeau (May 30 2018 at 17:21):

Matthieu Sozeau (May 31 2018 at 15:05):

@Aleksey Nogin found it and fixed it, this is a really good example exercising the mutual/nested/refinement combination, thanks!

Matthieu Sozeau (May 31 2018 at 15:05):

Aleksey Nogin (Gitter import) (May 31 2018 at 18:16):

Aleksey Nogin (Gitter import) (Jun 01 2018 at 14:57):

Any luck with that backport? Thanks! (travis timed out on 2nd-last fix98 commit, but seems like it succeeded on the last one).

Matthieu Sozeau (Jun 03 2018 at 18:01):

Matthieu Sozeau (Jun 05 2018 at 10:32):

Matthieu Sozeau (Jun 05 2018 at 10:47):

Jad Hamza (Gitter import) (Jun 05 2018 at 13:45):

@Matthieu Sozeau Thanks for looking into issue 96! Did you get a chance to look at https://github.com/mattam82/Coq-Equations/issues/75 ?
We have some examples where the "*_unfold_eq" Equations lemma take ~1 minute to prove

Matthieu Sozeau (Jun 05 2018 at 15:32):

Aleksey Nogin (Gitter import) (Jun 05 2018 at 19:20):

@Matthieu Sozeau Thanks a lot! The "production" definition now produces a Non strictly positive occurrence of "foo_ind" error - I will try to create a minimized version for a bug report

Aleksey Nogin (Gitter import) (Jun 05 2018 at 20:05):

Matthieu Sozeau (Jun 05 2018 at 20:10):

Thanks! I found one such issue when I started considering recursive calls under binders and fixed it, hopefully that one will go away as well

Matthieu Sozeau (Jun 06 2018 at 16:29):

Aleksey Nogin (Gitter import) (Jun 06 2018 at 23:13):

Thanks! Unfortunately, still getting an error with my current attempt at a "production" definition - filed mattam82/Coq-Equations#105.

Matthieu Sozeau (Jun 07 2018 at 07:57):

Matthieu Sozeau (Jun 07 2018 at 19:07):

@Aleksey Nogin indeed that was a duplicate, both #105 and #85 are fixed in 8.8 now

Aleksey Nogin (Gitter import) (Jun 07 2018 at 21:31):

Thanks! I am finally back to not having any blockers (at least none I am currently aware of)

Matthieu Sozeau (Jun 07 2018 at 21:54):

Aleksey Nogin (Gitter import) (Jun 08 2018 at 03:00):

I just filed mattam82/Coq-Equations#106 and mattam82/Coq-Equations#107 that have me confused even more than usual. The latter is the one I actually care about, the former is what I hit when intending to reproduce and report the latter. The difference in outcomes between the two and the error message in the latter have me particularly confused. It could be that I am once again not counting my arguments correctly, like I previously did with mattam82/Coq-Equations#100 - but I double-checked a few times (but it's also 8PM after a long day here, so who knows what I am missing)...

Matthieu Sozeau (Jun 08 2018 at 17:27):

@Aleksey Nogin Well, I fixed a bunch of things today, hopefully that lets you go further. Have a good week-end :)

Jad Hamza (Gitter import) (Jun 11 2018 at 07:58):

Matthieu Sozeau (Jun 11 2018 at 11:02):

@Jad Hamza there’s no way currently. I’ll have a look. It should be rather immediate given the technique we use, it must be reflexivity taking a very long time to check a convertibility.

Jad Hamza (Gitter import) (Jun 11 2018 at 11:37):

Jad Hamza (Gitter import) (Jun 11 2018 at 15:18):

@Matthieu Sozeau Thanks for fixing it! What do you mean by "the following lemma proof automation fails"?

Matthieu Sozeau (Jun 11 2018 at 15:20):

After the unfolding lemma there is the functional induction proof, which currently fails

Matthieu Sozeau (Jun 11 2018 at 15:21):

It can be proven by hand (it's a proof search failure when trying to use the admitted wf obligation proof) but then Coq anomalies because of a bug with obligations and universes

Jad Hamza (Gitter import) (Jun 11 2018 at 15:24):

@Matthieu Sozeau Ok I see, so I shouldn't upgrade coq-equations before Coq is upgraded to 8.8.1

Matthieu Sozeau (Jun 11 2018 at 15:25):

Jad Hamza (Gitter import) (Jun 11 2018 at 15:33):

@Matthieu Sozeau but then the lemmas won't pass anymore :) By the way when I do "opam upgrade coq-equations" it suggests I downgrade Coq to 8.7.2, is that normal?

Matthieu Sozeau (Jun 11 2018 at 15:43):

I don't think that's normal. If you do opam info coq-equations, what does it say?

Matthieu Sozeau (Jun 11 2018 at 15:44):

You can do [Next Obligation. apply admit. Defined] for that obligation to go further

Matthieu Sozeau (Jun 11 2018 at 15:45):

The functional elimination proof already failed before, even when you proved the unfolding lemma.

Jad Hamza (Gitter import) (Jun 11 2018 at 18:44):

Jad Hamza (Gitter import) (Jun 11 2018 at 18:46):

@Matthieu Sozeau In my current version, the functional elimination proof goes through: "FunctionalElimination_foldLeft is defined"

Matthieu Sozeau (Jun 11 2018 at 19:05):

Jad Hamza (Gitter import) (Jun 11 2018 at 19:07):

Matthieu Sozeau (Jun 11 2018 at 19:09):

Matthieu Sozeau (Jun 11 2018 at 19:10):

Jad Hamza (Gitter import) (Jun 11 2018 at 19:10):

Jad Hamza (Gitter import) (Jun 11 2018 at 19:14):

Matthieu Sozeau (Jun 11 2018 at 19:28):

Jad Hamza (Gitter import) (Jun 11 2018 at 19:29):

Matthieu Sozeau (Jun 11 2018 at 20:03):

Ah I checked because it bugged me. That's because the eliminator in 1.0 is weaker and actually useless. In the current branch the recursive call under the lambda is recognized and that's what makes the proof different.

Jad Hamza (Gitter import) (Jun 11 2018 at 20:05):

@Matthieu Sozeau 1.0 is the version that I'm using, which is old? Why don't I get the current branch with opam?

Matthieu Sozeau (Jun 11 2018 at 20:07):

That's because the development branches are in the extra-dev repository. Actually I'm missing an 8.8.dev package.

Jad Hamza (Gitter import) (Jun 11 2018 at 20:09):

@Matthieu Sozeau If I don't need these eliminators can I disable them? (I only need f_equation_1/2/3)

Matthieu Sozeau (Jun 11 2018 at 20:10):

Jad Hamza (Gitter import) (Jun 11 2018 at 20:11):

Jad Hamza (Gitter import) (Jun 11 2018 at 20:12):

Matthieu Sozeau (Jun 11 2018 at 20:13):

Could be. But actually if you have 1.0+88 installed then there's no reason to downgrade to 1.0+8.7

Matthieu Sozeau (Jun 11 2018 at 20:13):

Matthieu Sozeau (Jun 11 2018 at 20:14):

To add the opam repo you can simply do opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev

Matthieu Sozeau (Jun 11 2018 at 20:14):

Beware that it will likely eagerly select versions from this repo when you might prefer released packages in general

Jad Hamza (Gitter import) (Jun 11 2018 at 20:18):

Jad Hamza (Gitter import) (Jun 11 2018 at 20:24):

Matthieu Sozeau (Jun 11 2018 at 20:37):

Aleksey Nogin (Gitter import) (Jun 11 2018 at 22:33):

Is there a documentation for all the things Equations defines and how to use them? Am I supposed to use simp to replace an instance of an equation lhs with the corresponding rhs? I am having trouble where simp works for some equation-defined constructors and not for others (basically, referring to my issue reports, it seems to work correctly for the "production" version of "simp do_foo", and not do anything for the "production" version of "simp foo_type").

Aleksey Nogin (Gitter import) (Jun 12 2018 at 08:18):

I reported the issue I am having with simp in mattam82/Coq-Equations#111. I am currently blocked by mattam82/Coq-Equations#111 and mattam82/Coq-Equations#113...

Jad Hamza (Gitter import) (Jun 12 2018 at 08:27):

Hi @Matthieu Sozeau, is your fix for slow _unfold_eq part of the new 8.8.dev package?

Jad Hamza (Gitter import) (Jun 12 2018 at 08:28):

Jad Hamza (Gitter import) (Jun 12 2018 at 08:30):

Aleksey Nogin (Gitter import) (Jun 12 2018 at 08:30):

Jad Hamza (Gitter import) (Jun 12 2018 at 08:31):

Aleksey Nogin (Gitter import) (Jun 12 2018 at 08:33):

Yes, you would likely need to use the latest development version (I am using the latest v8.8 branch) - I reported and @Matthieu Sozeau fixed a bunch of bugs related to these kinds of definitions before I became able to get to this one.

Jad Hamza (Gitter import) (Jun 12 2018 at 08:37):

@Aleksey Nogin Ok I see. I'm not sure at all but I think simp works only on num but not on foo_type. simp num should replace num (List nil) by fun val => 0 for instance. (Similar to rewrite num_equation_1 in *, and num_equation_2, etc)

Aleksey Nogin (Gitter import) (Jun 12 2018 at 08:38):

Jad Hamza (Gitter import) (Jun 12 2018 at 08:39):

Aleksey Nogin (Gitter import) (Jun 12 2018 at 08:42):

Ah, sorry, "simp num" works once it actually have something to work on (my example does not get there). But still having the issue of not knowing how to rewrite foo_type(List l)

Aleksey Nogin (Gitter import) (Jun 12 2018 at 08:50):

Once that is solved, I would need to figure out how to set up a proper mutual induction that would enable me to actually prove the sample lemma.

Jad Hamza (Gitter import) (Jun 12 2018 at 09:04):

@Aleksey Nogin I compiled the 8.8 branch but I still cannot compile your example (fails on the struct keyword)

Aleksey Nogin (Gitter import) (Jun 12 2018 at 09:15):

Weird. Are you using an IDE? I somewhat regularly have issues with CoqIDE getting into a weird state and complaining about random things (like the struct keyword). Clicking the "restart Coq" button and then going back solves it - at least until it happens again.

Jad Hamza (Gitter import) (Jun 12 2018 at 09:25):

Jad Hamza (Gitter import) (Jun 12 2018 at 09:27):

@Aleksey Nogin intro. induction f. intros. simpl in *. unfolds the definition of foo_type (cbn instead of simpl works as well)

Aleksey Nogin (Gitter import) (Jun 12 2018 at 09:37):

@Jad Hamza - thanks, but unfortunately it looks like that was not the real issue - still no clue how to actually prove the lemma...

Aleksey Nogin (Gitter import) (Jun 12 2018 at 09:39):

I am currently trying ```Equations (struct f) num (f:foo) (val:foo_type f) : nat := {
num (List nil) val := 0;
num (List (cons hd tl)) val := sum hd (fun val => num hd val) tl val }
where (struct fs) sum (f:foo) (numf: (foo_type f -> nat)) (fs : list foo) (val: compact_prod (map foo_type (f::fs))) : nat := {
sum f numf nil val := numf val;
sum f numf (cons hd tl) val := numf (fst val) + sum hd (fun val => num hd val) tl (snd val)}.

Lemma num_zero: forall (f:foo) (val:foo_type f), num f val = 0. Check num_elim.
Proof. refine (proj1 (num_elim (fun f n v => v = 0) (fun f nf fs val s => s = 0) _ _ _ _)); intros; auto.

Matthieu Sozeau (Jun 12 2018 at 09:39):

@Aleksey Nogin for mutual induction you should probably call the eliminator using apply funelim (f:=num f) rather than doing an induction on f which doesn’t give you the right induction hypotheses for the List case.

Jad Hamza (Gitter import) (Jun 12 2018 at 09:41):

@Matthieu Sozeau I've tried your fix on the example for the issue and it works well, thanks! Unfortunately I have another example which is still very slow

Aleksey Nogin (Gitter import) (Jun 12 2018 at 09:41):

Matthieu Sozeau (Jun 12 2018 at 09:41):

Matthieu Sozeau (Jun 12 2018 at 09:43):

Matthieu Sozeau (Jun 12 2018 at 09:47):

Aleksey Nogin (Gitter import) (Jun 12 2018 at 09:49):

For funelim, this was the first thing I tried, but I have not figured out how I am supposed to call it. E.g.

Equations (struct f) num (f:foo) (val:foo_type f) : nat := {
  num (List nil) val := 0;
  num (List (cons hd tl)) val := sum hd (fun val => num hd val) tl val }
where (struct fs) sum (f:foo) (numf: (foo_type f -> nat)) (fs : list foo) (val: compact_prod (map foo_type (f::fs))) : nat := {
  sum f numf nil val := numf val;
  sum f numf (cons hd tl) val := numf (fst val) + sum hd (fun val => num hd val) tl (snd val)}.

Lemma num_zero (f:foo) (val:foo_type f): num f val = 0.
Proof. funelim (num f val).

In nested Ltac calls to "funelim" and "funelim_JMeq_tac", last call failed.

Matthieu Sozeau (Jun 12 2018 at 09:50):

Right. I didn't figure out yet how to make the tactic take additional predicates for mutual/nested definitions. So you have to call the eliminator directly like you did.

Aleksey Nogin (Gitter import) (Jun 12 2018 at 09:54):

Equations (struct f) num (f:foo) (val:foo_type f) : nat := {
  num (List nil) val := 0;
  num (List (cons hd tl)) val := sum hd (fun val => num hd val) tl val }
where (struct fs) sum (f:foo) (numf: (foo_type f -> nat)) (fs : list foo) (val: compact_prod (map foo_type (f::fs))) : nat := {
  sum f numf nil val := numf val;
  sum f numf (cons hd tl) val := numf (fst val) + sum hd (fun val => num hd val) tl (snd val)}.

Lemma num_zero: forall (f:foo) (val:foo_type f), num f val = 0. Check num_elim.
Proof. refine (proj1 (num_elim (fun f n v => v = 0) (fun f nf fs val s => (forall v, nf v = 0) -> s = 0) _ _ _ _)); intros; auto.
simpl in val. destruct val. simpl. rewrite H1. simpl in H0. rewrite H0; auto.

Aleksey Nogin (Gitter import) (Jun 12 2018 at 09:55):

Thanks a lot - I guess I will be able to figure it out from here - that is, once I know how to deal with mattam82/Coq-Equations#113...

Jad Hamza (Gitter import) (Jun 12 2018 at 09:58):

Matthieu Sozeau (Jun 12 2018 at 10:13):

Matthieu Sozeau (Jun 12 2018 at 10:15):

Jad Hamza (Gitter import) (Jun 12 2018 at 10:20):

Matthieu Sozeau (Jun 12 2018 at 10:22):

I would rather avoid doing pattern-matching in the right-hand side like here, although that's possible of course. About the slowness it seems that there is retypechecking taking a different conversion path which explodes again

Jad Hamza (Gitter import) (Jun 12 2018 at 10:26):

alright, thanks! It's anyways much faster than before your fix :) the style is indeed terrible but it's hard for us to do it differently since this is translated from another language. Or we would have to include some special cases than translate the pattern matching to a case analysis on the left hand side

Aleksey Nogin (Gitter import) (Jun 12 2018 at 17:39):

@Matthieu Sozeau Thanks so much for all the fixes - will hopefully be able to get my "production" code going again :smile: ! Just hoping I still have enough time to finish my "production" work in time for a big demo I have next Tuesday :worried: .

Aleksey Nogin (Gitter import) (Jun 12 2018 at 17:45):

Hm, Solving obligations automatically... seems to be getting stuck on one of my equations :( Will try to minimize/reproduce/report...

Matthieu Sozeau (Jun 12 2018 at 18:47):

@Anogin probably looping, that was reported already. Obligation Tactic := program_simplify might help.

Aleksey Nogin (Gitter import) (Jun 12 2018 at 23:30):

I reported mattam82/Coq-Equations#116 on nontermination and a potentially related mattam82/Coq-Equations#117 where a very similar code results in another Illegal Application. Obligation Tactic := program_simplify. does not seem to make any difference for the non-terminating example.

Aleksey Nogin (Gitter import) (Jun 13 2018 at 21:35):

Aleksey Nogin (Gitter import) (Jul 13 2018 at 03:38):

@Matthieu Sozeau: with all your fixes, I was able to finish all the proofs I wanted to do for an initial set of definitions I wanted to define - thanks so much!!! But now hit another issue with a new definition :( I filed mattam82/Coq-Equations#130.

Pierre Courtieu (Dec 07 2018 at 09:16):

Matthieu Sozeau (Dec 07 2018 at 12:15):

@Pierre Courtieu that's still on my list. I'm finishing a rewriting and cleanup of the Equations' handling of fixpoints (including nested well-founded ones) that should make the translation from a constrexpr/glob_constr to an input of Equations easier.

Pierre Courtieu (Dec 19 2018 at 16:40):

Jad Hamza (Gitter import) (Dec 21 2018 at 09:22):

Jad Hamza (Gitter import) (Dec 21 2018 at 09:44):

Require Import Equations.Equations.

Equations even (n: nat): Prop :=
  even n by rec n lt :=

  even 0 := True;
  even (S n) := odd n

where odd (n: nat): Prop :=
  odd n by rec n lt :=

  odd 0 := False;
  odd (S n) := even n
.

Here of course we don't need to use the custom by measures but in general is that supported?

Matthieu Sozeau (Dec 21 2018 at 10:39):

Nesting is supported but not mutual well-founded. For that you’d need an n-ary FixWf combinator. Using dependent pattern-matching you can encode it by defining even_odd (b : bool) (n : nat) : Prop though.

Jad Hamza (Gitter import) (Dec 21 2018 at 14:29):

Yannick Forster (Gitter import) (Apr 03 2019 at 13:42):

There was a question on Coq club where I wanted to jump in and say "Equations does exactly what you want!"... except it doesn't, at least not for me

Yannick Forster (Gitter import) (Apr 03 2019 at 13:42):

From Equations Require Import Equations.

Inductive eType : Set := Integer | Boolean.

Inductive unop : eType -> Type :=
  Neg : unop Integer
| Not : unop Boolean.

Lemma a : forall x : unop Integer, x = Neg.
Proof.
  intros. depelim x.

Yannick Forster (Gitter import) (Apr 03 2019 at 13:43):

I get H : {| pr1 := Integer; pr2 := x0 |} = {| pr1 := Integer; pr2 := Neg |} as assumption. That can be manually eliminated using EqDec.inj_right_pair, but that's somewhat unsatisfying

Yannick Forster (Gitter import) (Apr 03 2019 at 13:44):

Weirdly, if I do


Set Equations With UIP.
Axiom uipa : forall A, UIP A.
Existing Instance uipa.

before, that doesn't change anything

Yannick Forster (Gitter import) (Apr 03 2019 at 13:44):

Matthieu Sozeau (Apr 03 2019 at 13:46):

Matthieu Sozeau (Apr 03 2019 at 13:48):

depelim is an Ltac wrapper that does things a bit differently, trying to be closer to Program's depelim

Matthieu Sozeau (Apr 03 2019 at 13:49):

Yannick Forster (Gitter import) (Apr 03 2019 at 13:52):

Yannick Forster (Gitter import) (Apr 03 2019 at 13:53):

Jad Hamza (Gitter import) (Dec 05 2019 at 21:29):

Hello, is anyone able to use coq-equations master with coq master? I'm getting an error File not found on loadpath : equations_plugin.cmxs when trying to use coq master + coq-equations master (either compiled from source using make, or installed through opam with the dev versions) on files with equations

Jad Hamza (Gitter import) (Dec 06 2019 at 06:53):

(The file equations_plugin.cmxs does not appear at all in the folder of the dev opam switch)

Matthieu Sozeau (Dec 06 2019 at 14:38):

Jad Hamza (Gitter import) (Dec 07 2019 at 08:51):

Thanks! Aren't there continuous integration tests that make sure coq-equations master is always working with coq master?

Matthieu Sozeau (Dec 08 2019 at 11:19):

Matthieu Sozeau (Dec 08 2019 at 11:41):

@Jad Hamza indeed the install target was broken and only the vo's were installed, fixed now

Matthieu Sozeau (Dec 08 2019 at 11:42):

Jad Hamza (Gitter import) (Dec 08 2019 at 14:27):

Jad Hamza (Gitter import) (Dec 08 2019 at 14:36):

Matthieu Sozeau (Dec 08 2019 at 14:42):

Jad Hamza (Gitter import) (Dec 08 2019 at 14:52):

Mukesh Tiwari (Gitter import) (Dec 16 2019 at 01:39):

Require Import Equations.Equations.
Require Vectors.Vector.
Arguments Vector.nil {A}.
Arguments Vector.cons {A} _ {n}.
Notation vnil := Vector.nil.
Notation vcons := Vector.cons.

Equations prod {F G n}  (f : G -> F -> G) (g : G -> G -> G)
  (v : Vector.t G (S n)) (w : Vector.t F (S n)) :  G :=
  prod f g (vcons h nil) (vcons m nil) := f h m;
  prod f g (vcons h hs)  (vcons m ms)  :=
        g (f h m) (prod f g hs ms).

Mukesh Tiwari (Gitter import) (Dec 16 2019 at 01:40):

Mukesh Tiwari (Gitter import) (Dec 16 2019 at 01:41):

Error:
In environment
prod :
let H := fixproto in
forall (F G : Type) (n : nat),
(G -> F -> G) -> (G -> G -> G) -> Vector.t G (S n) -> Vector.t F (S n) -> G
F : Type
G : Type
f : G -> F -> G
g : G -> G -> G
h : G
m : F
ms : Vector.t F 0
hs := vnil : Vector.t G 0
The term "hs" has type "Vector.t G 0" while it is expected to have type "Vector.t G (S ?n)".

Paolo Giarrusso (Dec 16 2019 at 03:40):

Maybe a bug, but as a workaround I’d try to spell out the match against n and/or hs (and/or ms)

Paolo Giarrusso (Dec 16 2019 at 03:41):

the first line should match n against 0, the second against S n; it seems Equations fails to infer that

Mukesh Tiwari (Gitter import) (Dec 16 2019 at 04:05):

Equations prod {F G}  (f : G -> F -> G) (g : G -> G -> G)
          (n : nat) (v : Vector.t G (S n)) (w : Vector.t F (S n)) :  G :=
  prod f g 0 _ _ := _;
  prod f g (S n) (vcons h hs)  (vcons m ms)  :=
        g (f h m) (prod f g n hs ms).
Next Obligation.
  inversion_clear v;
    inversion_clear w.
  exact (f h h0).
Defined.

Mukesh Tiwari (Gitter import) (Dec 16 2019 at 05:52):

Mukesh Tiwari (Gitter import) (Dec 16 2019 at 05:53):

Equations prod {F G n}  (f : G -> F -> G) (g : G -> G -> G)
          (v : Vector.t G (S n)) (w : Vector.t F (S n)) : G :=
  prod (n := 0) f g (vcons m _) (vcons h _) := f m h;
  prod (n := (S n)) f g (vcons h hs) (vcons m ms)  :=
     g (f h m) (prod f g hs ms).

Matthieu Sozeau (Dec 16 2019 at 09:19):

Paolo Giarrusso (Dec 16 2019 at 11:00):

Matthieu Sozeau (Dec 16 2019 at 11:15):

Mukesh Tiwari (Gitter import) (Dec 16 2019 at 11:32):

Mukesh Tiwari (Gitter import) (Dec 16 2019 at 11:33):

Paolo Giarrusso (Dec 16 2019 at 12:19):

Matthieu Sozeau (Dec 16 2019 at 13:18):

Daniel Patterson (Gitter import) (Jan 02 2020 at 16:03):

Hi there -- I'm trying to use the mutual well-founded encoding described here: http://mattam82.github.io/Coq-Equations/examples/Examples.mutualwfrec.html -- but I'm running into issues with an error message "Too many patterns in clauses for this type" that I don't understand. I changed the provided example (the second encoding) relatively minimally to get the following reproduction:

Equations bmeasure (s : bool) (e : if s then nat else Z) : nat := {
bmeasure true e := e;
bmeasure false e := Z.to_nat e
}.

Karl Palmskog (Jan 02 2020 at 16:42):

Daniel Patterson (Gitter import) (Jan 02 2020 at 16:42):

Karl Palmskog (Jan 02 2020 at 16:43):

Karl Palmskog (Jan 02 2020 at 16:44):

Daniel Patterson (Gitter import) (Jan 02 2020 at 16:44):

Oh, shoot. Must be some other library interfering again -- I _was_ being careful about running these in isolation from the rest of the development but forgot in this case. Sorry!

Karl Palmskog (Jan 02 2020 at 16:44):

Daniel Patterson (Gitter import) (Jan 02 2020 at 16:48):

Daniel Patterson (Gitter import) (Jan 02 2020 at 16:52):

Paolo Giarrusso (Jan 02 2020 at 18:12):

Paolo Giarrusso (Jan 02 2020 at 18:14):

(On phone, but set implicit arguments might be marking that implicit automatically, causing confusion)

Daniel Patterson (Gitter import) (Jan 02 2020 at 20:30):

It doesn't work with s implicit (I assume you mean {s : bool}), whether Set Implicit Arguments is set or not.

Matthieu Sozeau (Jan 03 2020 at 10:10):

If you use {s} then indeed you have to give an explicit bmeasure (s:=true/false) in the clauses.

Karl Palmskog (Jan 03 2020 at 10:43):

is there a way to refer to (or specify the name of) the whole "superterm" of a pattern-matched parameter? E.g., I want to refer to S n' as only n in myeq (S n') := ...;

Karl Palmskog (Jan 03 2020 at 10:44):

the intuition is that in manual matches, I always have the name of the variable I match on

Karl Palmskog (Jan 03 2020 at 10:45):

one could imagine a syntax myeq n#(S n') := ..., or maybe I'm missing something

Paolo Giarrusso (Jan 03 2020 at 13:49):

Karl Palmskog (Jan 03 2020 at 14:12):

@Paolo G. Giarrusso indeed I tried this syntax, it doesn't work as far as I can tell

Karl Palmskog (Jan 03 2020 at 14:13):

unless @Matthieu Sozeau thinks otherwise I can write an issue with the feature request

Matthieu Sozeau (Jan 05 2020 at 03:50):

Yep it would be nice, sadly as is not part of the term grammar only the pattern one

Jakob Botsch Nielsen (Feb 12 2020 at 12:15):

Equations? egcd_aux (r0 a0 b0 r1 a1 b1 : bigZ) : Z * Z
  by wf (BigZ.log2 (BigZ.abs r0) + BigZ.log2 (BigZ.abs r1))
        (fun n m => 0 <= n < m) :=
egcd_aux r0 a0 b0 r1 a1 b1 with BigZ.div_eucl r0 r1 :=
  | (q, r) with dec (r =? 0) := {
    | left _ := ([a1], [b1]);
    | right _ := egcd_aux r1 a1 b1 r (a0 - q*a1) (b0 - q*b1)
  }.

How can I keep the equality BigZ.div_eucl r0 r1 = (q, r) around when proving that the measure is decreasing?

Matthieu Sozeau (Feb 12 2020 at 13:05):

You can use the "inspect" pattern by first defining a function inspect : forall {A} (a : A), { x : A | x = a } and pattern-matching on inspect (BigZ.div_eucld r0 r1)

Jakob Botsch Nielsen (Feb 13 2020 at 23:20):

Karl Palmskog (Feb 28 2020 at 12:36):

@Matthieu Sozeau any chance of a release of Equations for 8.11 in the near future?

Matthieu Sozeau (Feb 28 2020 at 12:53):

Karl Palmskog (Feb 28 2020 at 12:54):

Karl Palmskog (Feb 28 2020 at 13:00):

are there plans to do actual releases of coq-hott? It's not great to have a "stable" package have a depopt on an experimental package, this could potentially break at any time...

Karl Palmskog (Feb 28 2020 at 13:00):

Karl Palmskog (Feb 28 2020 at 13:19):

(for the record, the HoTT repo also takes a long, long time to clone, releases would elide this)

Bas Spitters (Feb 28 2020 at 20:32):

Karl Palmskog (Feb 28 2020 at 20:32):

Karl Palmskog (Feb 28 2020 at 20:33):

Bas Spitters (Feb 28 2020 at 20:34):

Bas Spitters (Feb 28 2020 at 20:35):

Karl Palmskog (Feb 28 2020 at 20:35):

Karl Palmskog (Feb 28 2020 at 20:36):

Bas Spitters (Feb 28 2020 at 20:36):

@Matthieu Sozeau, @alizter has been looking at hott equations. I believe his experiments were mostly positive.

Bas Spitters (Feb 28 2020 at 20:37):

Matthieu Sozeau (Mar 01 2020 at 12:45):

@Bas Spitters Cool, I just been fixing a bug on master for hott-equations. I should have a release for 8.11 upcoming as well. I'd love to have a stable hott package to depend on too :)

Matthieu Sozeau (Mar 01 2020 at 13:01):

Well, I can't release hott-equations until we have a coq-hott-8.11 package in fact

Bas Spitters (Mar 01 2020 at 13:08):

@Matthieu Sozeau I've asked @alizter to look into it. He's interning in Aarhus at the moment.

Jad Hamza (Gitter import) (Mar 07 2020 at 08:01):

Thanks for the Equations opam release for 8.11 :)
I noticed that simp f in * is in general slow compared to rewrite f_equation_1 in * || ... || rewrite f_equation_n in * (at least when f is marked Opaque), could it be that simp doesn't respect opacity?

Matthieu Sozeau (Mar 10 2020 at 13:14):

It might just be because simp f also calls typeclasses eauto with f after the autorewrite

Matthieu Sozeau (Mar 10 2020 at 13:15):

Jad Hamza (Gitter import) (Mar 10 2020 at 13:16):

Ah thanks, so I should write autorewrite with f if I want the same effect without eauto?

Matthieu Sozeau (Mar 10 2020 at 13:16):

Jad Hamza (Gitter import) (Mar 10 2020 at 13:18):

Jad Hamza (Gitter import) (Mar 10 2020 at 13:59):

Paolo Giarrusso (Mar 10 2020 at 14:11):

@Jad Hamza Hi! Assuming the lia change is not involved, autorewrite will iterate rewrites, like repeat rewrite; while your earlier code only rewrites once.

Jad Hamza (Gitter import) (Mar 10 2020 at 14:12):

Yes you're right that might cause the difference, but simp_red is often used within repeat

Jad Hamza (Gitter import) (Mar 10 2020 at 14:40):

Paolo Giarrusso (Mar 10 2020 at 14:43):

(any chance you need repeat also on the other variants of those tactics?) But Robbert Krebbers has complained about autorewrite performance a lot, but it being slower than repeat rewrite is surprising.

Paolo Giarrusso (Mar 10 2020 at 14:44):

Paolo Giarrusso (Mar 10 2020 at 14:45):

(maybe performance of autorewrite is best discussed in coq/coq? For instance, Jason Gross has been working on rewriting tactics and comparing with rewrite_strat)

Paolo Giarrusso (Mar 10 2020 at 14:49):

Paolo Giarrusso (Mar 10 2020 at 14:51):

that relies on Qed, which is actually Opaque, and it allows you to give a definition which is actually equal to its body only propositionally and not definitionally.

Jad Hamza (Gitter import) (Mar 10 2020 at 18:58):

Matthieu Sozeau (Mar 11 2020 at 12:45):

Matthieu Sozeau (Mar 11 2020 at 12:46):

Jad Hamza (Gitter import) (Mar 11 2020 at 12:52):

rewrite_strat indeed worked well! (and faster than repeat rewrite) after a few adjustments (importing RelationClasses and defining a few missing instances)

Paolo Giarrusso (Mar 11 2020 at 18:06):

@Jad Hamza oh, is rewrite_strat just faster or do you need to do optimizations yourself? I use Autosubst which uses autorewrite, and its performance is annoying

Jad Hamza (Gitter import) (Mar 11 2020 at 18:28):

I think it was faster out of the box (using this: https://github.com/epfl-lara/SystemFR/blob/7eff4ae12a8441001f49c58f3dea93758e78090f/ReducibilityDefinition.v#L213-L225), but I cannot tell for sure because some proofs didn't go through automatically and I had to do adjustments. There seems to be a difference with rewrite in *, which doesn't rewrite under binders while rewrite_strat maybe does? So I ended up using variants in these places such as simp_red_top_level_hyp, which will only rewrite top level occurrences. After all these changes (in commit https://github.com/epfl-lara/SystemFR/commit/7eff4ae12a8441001f49c58f3dea93758e78090f), the build using make -j10 went from around ~12min45 to ~11min20 (I didn't run these many times so these times may be off). Also, I didn't try other strategies (topdown or bottomup or innermost). Tell me your results if you try something :)

Paolo Giarrusso (Mar 11 2020 at 18:36):

Matthieu Sozeau (Mar 12 2020 at 09:44):

rewrite_strat uses congruence lemmas and produces smaller proof terms a priori, but indeed it's not 100% the same as autorewrite's strategy which is just repeat rewrite

Bas Spitters (Mar 15 2020 at 13:44):

Idris2 has some cool technology to generate programs from a type. Apparently, it originated here:
https://hackage.haskell.org/package/djinn
has anyone looked at porting it to Coq?

Paolo Giarrusso (Mar 15 2020 at 14:02):

isn’t that based on a foundation similar to tauto? if so, is there any significant difference in engineering?

Paolo Giarrusso (Mar 15 2020 at 14:06):

Bas Spitters (Mar 15 2020 at 14:43):

Yes, I think the basic algorithms are there, and one could hope that it can be put together cheaply, but I haven't looked into it deeply, as I would expect someone has done so already.

Karl Palmskog (Mar 15 2020 at 16:01):

Karl Palmskog (Mar 15 2020 at 16:02):

something like Isabelle's Nitpick would be more valuable, and solves a similar problem

Bas Spitters (Mar 15 2020 at 16:51):

Edwin referred to it as a "magic trick". Jasmin has been promising nitpick for DTT for some time, but I could find much progress. Do you happen to know more?

Karl Palmskog (Mar 15 2020 at 18:58):

Karl Palmskog (Mar 15 2020 at 18:59):

Karl Palmskog (Mar 15 2020 at 19:00):

it wouldn't surprise me if they do Lean integration first, since that's what Jasmin's current project targets

Bas Spitters (Mar 15 2020 at 20:29):

Karl Palmskog (Mar 15 2020 at 20:35):

Karl Palmskog (Mar 15 2020 at 20:37):

to be honest, I don't think any focused efforts will happen (w.r.t. counter-example generation and synthesis etc.) for Coq unless someone gets specific funds for it, I would say postdoc level for 1+ year or something like that

Karl Palmskog (Mar 15 2020 at 20:38):

Jasmin has one postdoc working on tools part-time (Gabriel Ebner), but my understanding is he mostly works on the hammer for Lean

Bas Spitters (Mar 15 2020 at 21:14):

Karl Palmskog (Mar 15 2020 at 21:21):

Karl Palmskog (Mar 15 2020 at 21:22):

I think the most design choices are in how to map the type theory to TPTP format and how to do reconstruction

Karl Palmskog (Mar 15 2020 at 21:23):

for CoqHammer, they (Kalizcyk and Csajka) chose to implicitly use an intermediate calculus "CIC0" and write custom reconstruction tactics

Karl Palmskog (Mar 15 2020 at 21:23):

Karl Palmskog (Mar 15 2020 at 21:25):

Karl Palmskog (Mar 15 2020 at 21:26):

Karl Palmskog (Mar 15 2020 at 21:28):

Théo Winterhalter (Mar 16 2020 at 14:56):

I’m trying to port an old project from coq 8.8 and I seem to have problems with Equations.
For instance

Derive NoConfusion for nat.

Solve Obligations tactic returned error: Tactic failure: Equations.Init.solve_noconf has not been bound yet.
This will become an error in the future [solve_obligation_error,tactics]

From Equations Require Import Equations.
Require Import Equations.Prop.DepElim.

Théo Winterhalter (Mar 16 2020 at 14:58):

I guess I’m missing something but I can’t figure it out. If someone knows, thanks. :)

Matthieu Sozeau (Mar 16 2020 at 15:38):

Théo Winterhalter (Mar 16 2020 at 15:39):

Cyril Cohen (Apr 15 2020 at 14:49):

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?

Matthieu Sozeau (Apr 15 2020 at 15:12):

PLBegay (Gitter import) (Apr 23 2020 at 14:08):

Hi everyone, when trying to install coq-equations 1.2+8.9 or 1.2.1+8.9 via opam on two different computers, I get an error (the sources couldn't be obtained, curl error code 500). I did add the https://coq.inria.fr/opam/released repo and I'm pretty sure it was working yesterday. Thanks in advance !

Paolo Giarrusso (Apr 23 2020 at 16:37):

@PLBegay releases are hosted on GitHub and GitHub was down. Please try again now that GitHub is up.

Stream: Equations devs & users

Topic: imported from gitter room coq/Equations

Pierre Courtieu (Jan 24 2018 at 14:51):

Pierre Courtieu (Jan 24 2018 at 14:51):

Matthieu Sozeau (Jan 25 2018 at 04:46):

Pierre Courtieu (Jan 25 2018 at 11:06):

Jad Hamza (Gitter import) (Apr 06 2018 at 11:34):

Jad Hamza (Gitter import) (Apr 06 2018 at 11:39):

Jad Hamza (Gitter import) (Apr 09 2018 at 11:45):

Matthieu Sozeau (Apr 12 2018 at 09:00):

Jad Hamza (Gitter import) (Apr 12 2018 at 11:01):

Jad Hamza (Gitter import) (Apr 13 2018 at 11:49):

Jad Hamza (Gitter import) (Apr 18 2018 at 18:09):

Matthieu Sozeau (Apr 19 2018 at 16:39):

Jad Hamza (Gitter import) (Apr 25 2018 at 12:48):

Matthieu Sozeau (Apr 25 2018 at 12:57):

Matthieu Sozeau (Apr 25 2018 at 12:57):

Jad Hamza (Gitter import) (Apr 25 2018 at 13:11):

Aleksey Nogin (Gitter import) (Apr 26 2018 at 17:50):

Aleksey Nogin (Gitter import) (Apr 27 2018 at 14:21):

Jad Hamza (Gitter import) (May 01 2018 at 05:18):

Aleksey Nogin (Gitter import) (May 01 2018 at 18:44):

Aleksey Nogin (Gitter import) (May 01 2018 at 20:55):

Aleksey Nogin (Gitter import) (May 02 2018 at 16:52):

Matthieu Sozeau (May 03 2018 at 12:19):

Aleksey Nogin (Gitter import) (May 03 2018 at 20:54):

Aleksey Nogin (Gitter import) (May 14 2018 at 16:49):

Aleksey Nogin (Gitter import) (May 14 2018 at 17:52):

Matthieu Sozeau (May 14 2018 at 18:04):

Matthieu Sozeau (May 14 2018 at 18:05):

Aleksey Nogin (Gitter import) (May 14 2018 at 18:09):

Matthieu Sozeau (May 14 2018 at 18:10):

Aleksey Nogin (Gitter import) (May 14 2018 at 18:17):

Matthieu Sozeau (May 14 2018 at 18:30):

Aleksey Nogin (Gitter import) (May 14 2018 at 18:31):

Matthieu Sozeau (May 14 2018 at 18:31):

Aleksey Nogin (Gitter import) (May 14 2018 at 18:33):

Aleksey Nogin (Gitter import) (May 14 2018 at 19:30):

Aleksey Nogin (Gitter import) (May 16 2018 at 15:54):

Matthieu Sozeau (May 16 2018 at 16:16):

Matthieu Sozeau (May 16 2018 at 16:39):

Aleksey Nogin (Gitter import) (May 16 2018 at 16:39):

Jad Hamza (Gitter import) (May 17 2018 at 12:54):

Jad Hamza (Gitter import) (May 17 2018 at 13:17):

Jad Hamza (Gitter import) (May 17 2018 at 13:21):

Matthieu Sozeau (May 17 2018 at 13:24):

Jad Hamza (Gitter import) (May 17 2018 at 13:27):

Matthieu Sozeau (May 17 2018 at 13:28):

Matthieu Sozeau (May 17 2018 at 13:29):

Jad Hamza (Gitter import) (May 17 2018 at 13:30):

Jad Hamza (Gitter import) (May 17 2018 at 13:31):

Jad Hamza (Gitter import) (May 17 2018 at 13:31):

Jad Hamza (Gitter import) (May 17 2018 at 13:31):

Jad Hamza (Gitter import) (May 17 2018 at 13:35):

Jad Hamza (Gitter import) (May 17 2018 at 13:37):

Matthieu Sozeau (May 17 2018 at 13:44):

Matthieu Sozeau (May 17 2018 at 13:45):

Matthieu Sozeau (May 17 2018 at 13:45):

Jad Hamza (Gitter import) (May 17 2018 at 13:47):

Matthieu Sozeau (May 17 2018 at 14:39):

Matthieu Sozeau (May 18 2018 at 16:27):

Jad Hamza (Gitter import) (May 23 2018 at 10:21):

Matthieu Sozeau (May 23 2018 at 12:57):

Jad Hamza (Gitter import) (May 23 2018 at 13:39):

Jad Hamza (Gitter import) (May 23 2018 at 13:42):

Matthieu Sozeau (May 23 2018 at 13:45):

Matthieu Sozeau (May 23 2018 at 13:47):

Jad Hamza (Gitter import) (May 23 2018 at 13:55):

Jad Hamza (Gitter import) (May 23 2018 at 14:03):

Matthieu Sozeau (May 23 2018 at 15:46):

Matthieu Sozeau (May 23 2018 at 15:46):

Matthieu Sozeau (May 23 2018 at 15:46):

Matthieu Sozeau (May 23 2018 at 15:47):

Aleksey Nogin (Gitter import) (May 23 2018 at 17:55):

Matthieu Sozeau (May 23 2018 at 18:01):

Aleksey Nogin (Gitter import) (May 23 2018 at 18:02):

Matthieu Sozeau (May 24 2018 at 12:12):

Aleksey Nogin (Gitter import) (May 29 2018 at 16:56):

Matthieu Sozeau (May 29 2018 at 17:43):

Aleksey Nogin (Gitter import) (May 29 2018 at 22:48):