imported from gitter room coq/coq · Coq devs & plugin devs

Hola Emilio! As for comparison to Mattermost and Slack, actually there is one here in the FAQ http://blog.gitter.im/2017/03/15/gitter-gitlab-acquisition/

Emilio Jesús Gallego Arias (Mar 28 2017 at 14:54):

indeed it could be useful for the reasons we mentioned

Emilio Jesús Gallego Arias (Mar 28 2017 at 14:55):

Yeah I think I fully trust you on the choice of particular chat room implementation

Emilio Jesús Gallego Arias (Mar 28 2017 at 14:55):

I have no preference other than it is easy for people to participate

Théo Zimmermann (Mar 28 2017 at 14:56):

Well Gitter certainly has this advantage over the others ^^

Emilio Jesús Gallego Arias (Mar 28 2017 at 14:56):

ok cool so let's stick to it for now

Emilio Jesús Gallego Arias (Mar 28 2017 at 14:56):

yeah in fact I think Maxime mentioned that

Emilio Jesús Gallego Arias (Mar 28 2017 at 14:57):

I just wanted to "announce" the room, I guess it was not the proper way xD

Théo Zimmermann (Mar 28 2017 at 14:57):

Well it kind of was a possible way, but I would have added a little text of explanation with the PR.

Emilio Jesús Gallego Arias (Mar 28 2017 at 14:57):

short on time these days xD

Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

but yeah, I guess the idea is to share some more conversations,

Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

these days all happens like

Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

one to one

Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

and it is very redudant

Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

if Travis break

Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

etc..

Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

and we where abusing the comment section of github a bit

Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

doing PRCHAT

Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

so this may help

Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

it may not XD

Théo Zimmermann (Mar 28 2017 at 14:59):

(I am always surprised when people post code without explanation, it kind of gives the message "this was discussed elsewhere already")

Théo Zimmermann (Mar 28 2017 at 14:59):

Anyways, I have been in a few Slacks before and the risk is having too much traffic for people to really follow.

Emilio Jesús Gallego Arias (Mar 28 2017 at 14:59):

the PR was my own thing XD

Théo Zimmermann (Mar 28 2017 at 14:59):

In which case, it may lead back to one-to-one conversations...

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:00):

we have been indeed discussing for some months about the 1-1 chat problem

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:00):

ok let's see how this works

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:00):

I am not a user myself of IRC

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:00):

since 1997

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:00):

or so

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:00):

yeah I found it hard to follow

Théo Zimmermann (Mar 28 2017 at 15:00):

As for myself, I am only a very occasional user. I'm not really accustomed to it.

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:01):

yeah so lets try to keep the chat efficient

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:01):

I guess people is not really supposed to follow this

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:01):

in the sense

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:01):

that relevant issues

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:01):

will be always get a bug or a PR

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:02):

but indeed a few things can be helpful

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:02):

questions

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:02):

this kinda overlaps with coqdev

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:02):

I dunno

Théo Zimmermann (Mar 28 2017 at 15:02):

yes it does

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:02):

this is why I always refused to use gitter

Théo Zimmermann (Mar 28 2017 at 15:02):

as much as SO overlaps with coq-club

Théo Zimmermann (Mar 28 2017 at 15:02):

but still I prefer SO to coq-club

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:02):

but lets be open

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:02):

yeah I know what you man

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:02):

mean

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:03):

subtle details in the interface

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:03):

do make a big difference

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:03):

hihi

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:03):

this is maybe a good forum

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:03):

to discuss about which PR

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:03):

should be fast-tracked

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:04):

obligatory bash.org quote: http://www.bash.org/?4281

Théo Zimmermann (Mar 28 2017 at 15:04):

I would advise finishing one's sentence before sending it though, because otherwise only a very short column of my screen is actually useful. Besides, line-wrapping exists if one has a smaller window. Yeah, I know I made this message very long on purpose.

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:05):

dedicated to the release manager

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:05):

sure sorry about that!

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:05):

I'll stop the useless chat

Théo Zimmermann (Mar 28 2017 at 15:05):

Théo Zimmermann (Mar 28 2017 at 15:08):

Do you see the coq/travis chat room I have created?

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:09):

I had to click in "more coq rooms"

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:09):

and join

Théo Zimmermann (Mar 28 2017 at 15:10):

OK, I figured it would make sense to have special topic rooms, what do you think?

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:11):

Maybe for Travis it does, but IMVHO I'd keep it simple for now, we will struggle just to use one room I guess

Théo Zimmermann (Mar 28 2017 at 15:11):

Théo Zimmermann (Mar 28 2017 at 15:13):

@Emilio Jesús Gallego Arias I already see a good use to this Gitter. Which is to ask you what do you think about my draft-CEP on the stdlib?

Théo Zimmermann (Mar 28 2017 at 15:13):

I wouldn't have sent an e-mail just to ask this. Nor a new comment on GitHub.

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:18):

It looks cool

Théo Zimmermann (Mar 28 2017 at 15:18):

:smile:

Théo Zimmermann (Mar 28 2017 at 15:20):

I think I'll propose it for acceptance at the next WG, in the meantime it would be good if it could gather a few more comments to make it better.

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:20):

I'm all for it, right now it is very hard to evolve libraries as you noted. I hope it can land in 8.7. In fact, in one of my first Coq working group I proposed to split the stdlib , see https://coq.inria.fr/cocorico/CoqDevelopment/CoqWG20160216

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:21):

However, it was met with particular resistance. I believe @letouzey provided some good arguments against it, so I focused towards trying to split coqide and coqchk which is imho more feasible

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:22):

So in fact, the first time I heard about splitting the libs was in the first coding sprint, but again mostly of it was random coffee chat

Théo Zimmermann (Mar 28 2017 at 15:22):

Yes, I know that he has been in favor of splitting just a part of the library (Reals mostly)

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:23):

So summarizing, I love the idea, however the devil is on the details. Actually realizing the implementation may prove tricky

Théo Zimmermann (Mar 28 2017 at 15:23):

So there is also this question of splitting the lib in several parts but I think it makes sense to postpone it and first concentrating on extracting the whole thing and test the development model we can have with it.

Théo Zimmermann (Mar 28 2017 at 15:25):

Some of the tricky points are listed in "Unresolved questions". If you see more, let me know.

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:25):

let me have a fresh look to it

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:27):

for one, I can help with co-driving the CEP [random note, I find this CEP process a bit painful, maybe we could just use GH's wiki?]

Théo Zimmermann (Mar 28 2017 at 15:28):

Cool, thanks! I'll add you to the drivers.

Théo Zimmermann (Mar 28 2017 at 15:28):

I'm not convinced that wikis are good for discussion. They are good to create TODO lists though.

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:29):

I am not a fan either, it is just that modifyin some stuff on the PRs is a bit painful, maybe I have the rights to push commits?

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:29):

So the initial idea looks good IMO

Théo Zimmermann (Mar 28 2017 at 15:30):

Actually I think that you have the rights to push some commits to this branch.

Théo Zimmermann (Mar 28 2017 at 15:30):

Because you are a maintainer of the repository (I think) and I checked the "Allow edits from maintainers" box.

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:30):

In this quick read I am only missing one point, what about git versioning? For instance, you may need to specifiy constraitns such as lib \gt 2.8.3+git-22-abcd283

Théo Zimmermann (Mar 28 2017 at 15:31):

Can you try e.g. pushing a commit to move your name in the drivers list?

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:31):

I am not an admin on that repository

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:34):

yeah it is missing from the team page, likely an oversight of the admins @Maxime Dénès

Théo Zimmermann (Mar 28 2017 at 15:34):

You're one of the only two "core developers" who is not an "owner" of the Coq organization so I suppose you don't have the permissions to add yourself as a maintainer on that repository.

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:35):

Yeah, I think the problem is that the repository itself is not properly set up

Théo Zimmermann (Mar 28 2017 at 15:35):

Ah OK

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:35):

the coq-ceps I mean

Théo Zimmermann (Mar 28 2017 at 15:38):

Back to the git versioning question, I suppose we could wait and see the use cases. But that's indeed an interesting question to keep in mind. Feel free to add it to the list.

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:40):

I find myself depending on particular Coq versions as PR are merged and APIs are improved etc... so it would make sense to have finer bounds. git describe seems to work well, as discussed in coq/coq#483 (and also there has been some private discussion)

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:40):

Yeah, at least here, if we chat, you don't need to pay attention, but later on, I can refer you to the archive of the discussion!

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:50):

I am gonna test the GH integration

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:50):

of course we can disable it afterwards, let's see what it does

Emilio Jesús Gallego Arias (Mar 28 2017 at 15:52):

Ups, it needs write authorization to coq/coq, so even if I can do it I'd rather get approval from the coq repos owner. A cool thing thou is that we could add another chat room and add notifications for all coq-related commits, including plugins etc...

Maxime Dénès (Mar 28 2017 at 16:13):

@Emilio Jesús Gallego Arias let me know if need something

Emilio Jesús Gallego Arias (Mar 28 2017 at 16:13):

@Maxime Dénès are you ok with enabling the github hooks for gitter?

Maxime Dénès (Mar 28 2017 at 16:13):

does it really require write access? I thought it was only for private repos

Emilio Jesús Gallego Arias (Mar 28 2017 at 16:14):

it requires adding a hook to the coq repos

Emilio Jesús Gallego Arias (Mar 28 2017 at 16:14):

that is

Emilio Jesús Gallego Arias (Mar 28 2017 at 16:14):

so write access to the hooks folder, I guess pretty harmless, but not something to do own my own, you can enable it very quickly if you want clicking in the integration menu

Emilio Jesús Gallego Arias (Mar 28 2017 at 16:32):

by the way @Maxime Dénès I think the coq/coq-ceps repository is wrongly configured permission-wise on GitHub

Maxime Dénès (Mar 28 2017 at 18:02):

does the write access need to stay?

Maxime Dénès (Mar 28 2017 at 18:02):

or is it just for setting it up?

Emilio Jesús Gallego Arias (Mar 28 2017 at 18:04):

it is just for setting up I guess

Maxime Dénès (Mar 28 2017 at 18:09):

it should be ok

Maxime Dénès (Mar 28 2017 at 18:09):

no need to give write access in fact

Emilio Jesús Gallego Arias (Mar 28 2017 at 18:10):

the side panel is cool, as seen in coq/travis

Maxime Dénès (Mar 28 2017 at 18:10):

btw there is a Travis integration as well

Maxime Dénès (Mar 28 2017 at 18:10):

I could set that up

Emilio Jesús Gallego Arias (Mar 28 2017 at 18:11):

$\forall P : Prop , P$

Emilio Jesús Gallego Arias (Mar 28 2017 at 18:11):

@Théo Zimmermann set it up in the travis room

Emilio Jesús Gallego Arias (Mar 28 2017 at 18:11):

I personally have no opinion on the room structure

Emilio Jesús Gallego Arias (Mar 28 2017 at 18:11):

I think the travis room makes sense

Maxime Dénès (Mar 28 2017 at 18:12):

coq/travis?

Emilio Jesús Gallego Arias (Mar 28 2017 at 18:12):

yeah, I don't know how to reference a room

Théo Zimmermann (Mar 28 2017 at 19:38):

About the discoverability of rooms: world icon in the top-right corner

Emilio Jesús Gallego Arias (Mar 29 2017 at 08:01):

You know folks who will be my hero? Whoever makes us move away from bugzilla xD

Maxime Dénès (Mar 29 2017 at 08:17):

what would you use instead?

Emilio Jesús Gallego Arias (Mar 29 2017 at 08:19):

even debbugs would be better XD

Emilio Jesús Gallego Arias (Mar 29 2017 at 08:21):

I don't know, it is a hard question, I am becoming very lazy these days so even github issues could work, but certainly something that could integrate with source code such as trac, or phabricator, etc...

Emilio Jesús Gallego Arias (Mar 29 2017 at 08:21):

Oh we have the activity at the side! It looks very cool!

Théo Zimmermann (Mar 29 2017 at 10:46):

Well, I would use GitHub's issues. But as I said before, I'm not going to push for it. I would be interested though to have a precise list of the features of Bugzilla that are deemed useful and see how these can be replaced.

Emilio Jesús Gallego Arias (Mar 29 2017 at 10:56):

Interesting point, for me I don't see any advantage... I can't edit comments, properly format them, neither modify the issues. Théo, are you happy with Bugzilla?

Maxime Dénès (Mar 29 2017 at 11:55):

spread the word: each time you use apply, a kitten does in atrocious cruelties

Emilio Jesús Gallego Arias (Mar 29 2017 at 11:55):

you gotta be careful with application

Emilio Jesús Gallego Arias (Mar 29 2017 at 11:55):

that was a highly controversial at OPLSS 2013

Emilio Jesús Gallego Arias (Mar 29 2017 at 11:56):

would you like to deprecate it? (in favor of refine ........)

Emilio Jesús Gallego Arias (Mar 29 2017 at 11:56):

how many things would break?

Emilio Jesús Gallego Arias (Mar 29 2017 at 11:57):

I remember the last argument I heard was that apply was doing some useful 2nd-order unification thing

Maxime Dénès (Mar 29 2017 at 12:03):

you don't want to know :smile:

Emilio Jesús Gallego Arias (Mar 29 2017 at 12:06):

oh well it would be useful, IIRC for evarcons it was the case that due to the bug

Emilio Jesús Gallego Arias (Mar 29 2017 at 12:07):

the set of constraints was ordered differently

Emilio Jesús Gallego Arias (Mar 29 2017 at 12:07):

then we got different solutions, sometimes weaker, sometimes stronger, right?

Emilio Jesús Gallego Arias (Mar 29 2017 at 12:07):

what is the bug doing to unification.ml?

Emilio Jesús Gallego Arias (Mar 29 2017 at 12:08):

because the only thing that econstr can do is to expose critical bugs

Emilio Jesús Gallego Arias (Mar 29 2017 at 12:09):

as you know I'm really against the terminology "normal form" wrt evars

Emilio Jesús Gallego Arias (Mar 29 2017 at 12:09):

such a thing doesn't exist, there is only one form possible

Théo Zimmermann (Mar 29 2017 at 13:15):

@Emilio Jesús Gallego Arias No not happy at all with Bugzilla! I can't subscribe to the new bugs, I don't have the right set of permissions to change anything to a bug, including assigning myself, unless I was the OP.

Théo Zimmermann (Mar 29 2017 at 13:16):

While if we had bugs on GitHub we could have commit messages saying "This closes #3405850" and this would close the issue when the commit is merged. \o/

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:17):

Théo Zimmermann (Mar 29 2017 at 13:18):

@Emilio Jesús Gallego Arias I'm not going to answer you on the CEP PR because that's precisely what I wanted to avoid.

Théo Zimmermann (Mar 29 2017 at 13:18):

But I can answer you here.

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:19):

So we could try to discuss again at the WG. I would support the move to GitHub bugs, but not very enthusiastically as bug data is crucial and I am not sure how open the system is.

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:19):

Oh please

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:19):

answer here

Théo Zimmermann (Mar 29 2017 at 13:20):

Just to finish on this bugs discussion first, yes I'm not strongly advocating for the move because it would have much larger implications than just making GitHub the main repo and we can see as just this seems so complicated!

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:21):

Paradoxically the repository issue is not so complicated in my view, in the sense that migrating a repository is a one-minute thing

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:22):

however migrating a bug tracker, is huge. It is just that bugzilla is painful

Théo Zimmermann (Mar 29 2017 at 13:22):

I know! And it's not complicated in my view either. It's even fully reversible.

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:22):

maybe we should just poll support for Bugzilla first

Théo Zimmermann (Mar 29 2017 at 13:22):

But people are still arguing against the move. I can't understand why.

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:22):

and then try to build another replacement

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:22):

but oh man

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:22):

this is not Coq

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:22):

it is more like a Turtle

Théo Zimmermann (Mar 29 2017 at 13:23):

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:23):

I can't understand why.
political reasons

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:23):

I can understand why

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:23):

where to host the code has IMO important political significance

Théo Zimmermann (Mar 29 2017 at 13:23):

Yeah but political reasons are used in a inconsistent fashion

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:23):

that's intrinsic to politics, isn't it ?

Théo Zimmermann (Mar 29 2017 at 13:23):

e.g. where we accept PRs is more important and as many more implications

Théo Zimmermann (Mar 29 2017 at 13:24):

it is, yes

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:24):

a very experienced politician told me once "politics is very easy: here are your friends, here are your enemies"

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:24):

anyways

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:24):

so what about the CEP?

Théo Zimmermann (Mar 29 2017 at 13:26):

Not really about the CEP but more on the SSR discussion, I wouldn't mind if SSR authors preferred to have a different namespace than just Coq, but keeping math-comp makes little sense to me because it is sending the message: this is still a little part of math-comp, it's just distributed with Coq.

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:26):

well it is tightly couple AFAICT

Théo Zimmermann (Mar 29 2017 at 13:26):

But if it's really just what we want, then no need of a PR for this.

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:26):

in the same way ring and reals are

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:27):

I would rather say

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:27):

"this is a part of mathcomp, which has become a part of Coq"

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:27):

many things were outside

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:27):

like Program / Obligation

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:27):

and now are "inside"

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:27):

so imagine the case for Program

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:27):

if includes were of the from

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:28):

From Program Require XX

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:28):

Why to change it when it was merged?

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:28):

I like namespaces, so this is a very personal opinion

Théo Zimmermann (Mar 29 2017 at 13:28):

Well now it is From Coq Require Program.XX

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:28):

But again I think that the problem here is what is the definition of "being part of Coq"

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:29):

so far it was "it is in the main repository" but that will change with your PR

Théo Zimmermann (Mar 29 2017 at 13:29):

anyways, that math-comp become a part of Coq has not been proposed

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:29):

in fact I have an even wider view, in the sense that, for instance, in jscoq

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:29):

every time the user types "From XXX Require UU"

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:29):

it will donwload it

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:29):

and all the packages will live in the same namespace

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:30):

I find it absurd that we have to "install" things these days

Théo Zimmermann (Mar 29 2017 at 13:30):

oh I fully agree with you on that point

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:30):

I just want things to work; I guess I am lazy, not as lazy as the Coq-Turtle but close

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:30):

for me the "being part of Coq" has become a bit meaningless , in the same way than to say "being part of C++"

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:31):

there are things that are officially supported

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:31):

either by the Coq Developers

Théo Zimmermann (Mar 29 2017 at 13:31):

Well, you were not the one proposing it anyways

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:31):

or by other persons

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:31):

I just don't care

Théo Zimmermann (Mar 29 2017 at 13:31):

so I suppose @gares and @Maxime Dénès have other views.

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:31):

I am a programmer, I just want all my libraries to be there, like OPAM

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:32):

in opam I usually don't care about the provenance

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:32):

I just say "i need this" and I get what I want

Théo Zimmermann (Mar 29 2017 at 13:33):

Yes, I know what you mean. But we're not getting very far in the discussion since you're obviously not sharing the views of the people who proposed the integration.

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:33):

and we spend lots and lots of time about these discussion, that may be very interesting for some people, but I just don't care, and people using ssreflect just care about having it in the default package, that is

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:33):

Here I don't share any view, it is just that somehow my brain blocks on this sorry XD

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:35):

I cannot get my brain to even form a view; it is like an irrelevant issue for me; I think of that and we have spent many many hours discussing about these topics, whereas other many core parts of the system are truly in need of work. As I said, if was the release manager I would have just merged math-comp in 2 minutes, and move on to other things. So yeah, sorry for that XD

Théo Zimmermann (Mar 29 2017 at 13:35):

Anyways, that's quite easy to have SSReflect be distributed in the same package as Coq. That wouldn't require changing the development model. Conversely, in the CEP I'm proposing changing the development model of the standard library, but not how it's distributed.

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:35):

Well, anyways the point was that IMHO I like top-level namespaces

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:36):

And IMHO you need them

Théo Zimmermann (Mar 29 2017 at 13:37):

Sure well, listen it was just an example I was taking randomly. To show @silene that moving things in or moving things out, the issues at stake should be exactly the same. No more no less.

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:44):

Yeah, just to conclude on that, IMO ssreflect.v should be kept under the math-comp prefix. ssr2, indeed, could be put in a different one. I guess that is what got me confused.

Emilio Jesús Gallego Arias (Mar 29 2017 at 13:44):

they won't be compatible

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:51):

Emilio Jesús Gallego Arias can I merge #525 now?

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:51):

@Maxime Dénès sure I think so

Maxime Dénès (Mar 29 2017 at 15:51):

oups sorry

Maxime Dénès (Mar 29 2017 at 15:51):

wrong channel

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:52):

the perils of "manual" serialization. It is funny than in all my printing cases I never found an empty thing

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:52):

yeah I though this could go to the main one right?

Maxime Dénès (Mar 29 2017 at 15:52):

sure

Maxime Dénès (Mar 29 2017 at 15:53):

I'll do a pass of merges later tonight

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:53):

great

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:53):

I have little on the queue

Maxime Dénès (Mar 29 2017 at 15:53):

I'm launching a benchmark of EConstr, we finally solved the last known issues

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:53):

that's great

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:53):

I saw your latest push

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:54):

PR wise I'd really like to get merged #441, and then I am done for a while, but this needs Enrico OK and I understand he may need some extra time

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:54):

so that should be OK

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:54):

#441 will likely introduce some minor annoyances

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:55):

maybe the toplevel shows goals in differente cases

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:55):

but all of that should be minor

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:55):

again it is hard to test interactive behavior

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:55):

also #552 should be safe to merge, this was an omission on my part

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:55):

wrt to CoqIDE however

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:56):

the new goal display needs some help from people knowlegde in GTK

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:56):

if we don't like it, it is easy to go back

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:56):

the main difference is that now

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:56):

at every size change, coqide will repaint the goal window

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:56):

previously, it only repainted when sending a command

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:58):

so it is easy to go back if we don't like the new model. I like the new model, but however I fail to implement some nice features, like having the repaint preserve the scroll status. I tried some hacks but they are ugly. Not to say that my impression of GTK is extremly negative. Many years ago I had a look at the code (in particular the GTK notebook code) and I was extremely horrified, so many obvious bugs (like not checking null pointers) that I had to stop midway. I wouldn't pass a student writing that code.... so it could be well the case that that the cool stuff is actually hard to program without ugly hacks.

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:59):

Anyways I'll try to improve the window display a bit more in the summer, after I ask a few questions on the gtk mailing list.

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:59):

on the other hand, it is very likely that we have news soon for some new ide efforts

Emilio Jesús Gallego Arias (Mar 29 2017 at 15:59):

vscode is free software and runs reasonably well

Emilio Jesús Gallego Arias (Mar 29 2017 at 16:00):

and I heard some rumours of an atom IDE being prepared by crazy people XD

Emilio Jesús Gallego Arias (Mar 29 2017 at 16:01):

also #502 should be IMHO merged

Emilio Jesús Gallego Arias (Mar 29 2017 at 16:03):

So that is my queue:

kinda trivial: #502 #506 #522 #525
ready for this round: #511 #461 (if desired)
IMO OK but waiting for @silene and maybe @ppedrot approval: #512
Ready but waiting for @gares: #441

Emilio Jesús Gallego Arias (Mar 29 2017 at 16:05):

that's all

Emilio Jesús Gallego Arias (Mar 29 2017 at 16:08):

my next PR will be the refactoring of the STM state, it will be a largish commit , however I don't expect it to affect any plugins or users. Also, I expect it will really help with many current problems, in particular, the way we traverse nodes now it is very delicate as every traversal will restore the cached state, and sometimes you don't want that. I lost two days tracking why parsing was failing in jscoq, until I realized that simply checking for the readiness of a state will set you back in time. In fact, I wonder whether bug#5423 could be realted

Emilio Jesús Gallego Arias (Mar 29 2017 at 16:08):

seems exaclty like that

Emilio Jesús Gallego Arias (Mar 29 2017 at 16:43):

by the way folks @Maxime Dénès @Théo Zimmermann , maybe you would like to announce the gitter to coqdev, maybe just as "an experiment" I guess not all people are as careful as zimmi and saw the PR. I am sure some people will also object, but on the other hand I am not sure a strong argument against this kind of tool can be made.

Théo Zimmermann (Mar 29 2017 at 17:20):

So you have tested vscode. It has been in my TODO list for a while.

Théo Zimmermann (Mar 29 2017 at 17:21):

I got the impression that Paul was saying that CJ was leaving the team (at MIT I suppose) and he feared that he wouldn't support it anymore but it seem to have recent commits.

Théo Zimmermann (Mar 29 2017 at 17:22):

well maybe 24 days ago is not so recent

Emilio Jesús Gallego Arias (Mar 29 2017 at 17:28):

The question is that the day that supporting vscode is easier than supporting CoqIDE may be soon. Also, IMHO the vscode binding is extremely complicated due to the stateful protocol, but much of its complexity could be eliminated by switching it to other protocol

Emilio Jesús Gallego Arias (Mar 29 2017 at 17:30):

ms-ide-protocol support for serapi is not far, also, the implementation of term rendering can be shared by jscoq, atom and vscode

Emilio Jesús Gallego Arias (Mar 29 2017 at 17:30):

so indeed

Emilio Jesús Gallego Arias (Mar 29 2017 at 17:31):

pity we didn't have the manpower to submit the GSOC again for 2017

Théo Zimmermann (Mar 29 2017 at 17:32):

oh really that deadline passed? :(

Théo Zimmermann (Mar 29 2017 at 17:33):

I couldn't have helped much anyways, but I fully support your efforts in this general direction.

Maxime Dénès (Mar 29 2017 at 20:44):

do you guys know if there's any plan to get better debugging tools in the OCaml ecosystem?

Emilio Jesús Gallego Arias (Mar 29 2017 at 21:20):

That would be a good topic for the ocaml room. I have no clue, I'm sure Jane Street ought to be cooking something given the size of their codebase. I will just say than a few times I've found easier to transpile Coq to Javascript and use the JS debugger there than to try to debug ocaml directly XD

Emilio Jesús Gallego Arias (Mar 29 2017 at 21:40):

@Théo Zimmermann I've submitted https://coq.inria.fr/bugs/show_bug.cgi?id=5426 about bugzilla permissions, you may want to weigth in

Maxime Dénès (Mar 29 2017 at 21:54):

I have a feeling that the maintenance strategy for CoqIDE is something we will have to discuss in a not-so-distant future

Emilio Jesús Gallego Arias (Mar 29 2017 at 21:55):

Well, what the options are? I would certainly split it from Coq. Thanks to work started in Nice 2015 it is totally self-contained see ejgallego/coqide-exp

Emilio Jesús Gallego Arias (Mar 29 2017 at 21:55):

https://github.com/ejgallego/coqide-exp

Emilio Jesús Gallego Arias (Mar 29 2017 at 21:55):

so at least we are good here

Emilio Jesús Gallego Arias (Mar 29 2017 at 21:56):

in fact, toplevel wise Coq is totally modular now and ocambuild is already building it as modules (there's a trivial circular dependency but I'll get to submit a PR some of these days)

Emilio Jesús Gallego Arias (Mar 29 2017 at 21:56):

this is IMO nice as all the clients build modularly now

Emilio Jesús Gallego Arias (Mar 29 2017 at 21:56):

both the jscoq and serapi toplevel build this way

Emilio Jesús Gallego Arias (Mar 29 2017 at 21:57):

and they workaround many problems the current build system has, including difficulty to build with external dependencies

Emilio Jesús Gallego Arias (Mar 29 2017 at 21:57):

and you can just build against the kernel if you do package(coq.kernel) etc...

Emilio Jesús Gallego Arias (Mar 29 2017 at 21:58):

I do think that splitting CoqIDE has many benefits

Maxime Dénès (Mar 29 2017 at 21:58):

yeah I had to include ppx_deriving as a dependency for Paul, it was a nightmare because you need to remove all the manual references to unix.cmxa that are there today

Emilio Jesús Gallego Arias (Mar 29 2017 at 21:58):

yeah that is not worth it

Emilio Jesús Gallego Arias (Mar 29 2017 at 21:58):

I have somewhere in my hard disk a patch that builds coqtop using the serapi build system, have a look how easy it is: https://github.com/ejgallego/coq-serapi/blob/master/_tags

Maxime Dénès (Mar 29 2017 at 21:59):

Well it was painful, but it took me like 30 minutes. The diagnosis in unification.ml for EConstr took me 2 days and 1 night...

Emilio Jesús Gallego Arias (Mar 29 2017 at 21:59):

but about CoqIDE

Emilio Jesús Gallego Arias (Mar 29 2017 at 21:59):

well, try to link more advanced stuff and you will see

Emilio Jesús Gallego Arias (Mar 29 2017 at 21:59):

anyways, about CoqIDe

Maxime Dénès (Mar 29 2017 at 21:59):

does it build the VM?

Emilio Jesús Gallego Arias (Mar 29 2017 at 21:59):

it would greatly benefit from independent releases

Emilio Jesús Gallego Arias (Mar 29 2017 at 21:59):

and of having easy branching

Emilio Jesús Gallego Arias (Mar 29 2017 at 21:59):

branches

Emilio Jesús Gallego Arias (Mar 29 2017 at 22:00):

well, that is for building against a normally built Coq

Emilio Jesús Gallego Arias (Mar 29 2017 at 22:00):

but my ocamlbuild tree indeed does build the VM

Emilio Jesús Gallego Arias (Mar 29 2017 at 22:00):

let me see the status of that

Emilio Jesús Gallego Arias (Mar 29 2017 at 22:01):

well it is in a mess now, a mix of the old approach of Pierre plus hacks https://github.com/ejgallego/coq/blob/ocamlbuild/myocamlbuild.ml

Emilio Jesús Gallego Arias (Mar 29 2017 at 22:01):

but it does work

Emilio Jesús Gallego Arias (Mar 29 2017 at 22:01):

just needs polishing, no special difficulty

Emilio Jesús Gallego Arias (Mar 29 2017 at 22:02):

anyways ocamlbuild is slower for Coq, but it is interesting as a build option

Emilio Jesús Gallego Arias (Mar 29 2017 at 22:02):

as you can use it to build the upper layers

Emilio Jesús Gallego Arias (Mar 29 2017 at 22:02):

coqide, etc..

Emilio Jesús Gallego Arias (Mar 29 2017 at 22:02):

which don't really benefit from paralellism

Emilio Jesús Gallego Arias (Mar 29 2017 at 22:02):

and build the lower layers the usual way

Emilio Jesús Gallego Arias (Mar 29 2017 at 22:02):

the cma in the META files

Maxime Dénès (Mar 29 2017 at 22:02):

the discussion on #485 is too long for me. Can you summarize? I.e. is it ready for merge?

Emilio Jesús Gallego Arias (Mar 29 2017 at 22:03):

IMO it needs the OK of Clément and @matafou

Emilio Jesús Gallego Arias (Mar 29 2017 at 22:03):

that is to say

Emilio Jesús Gallego Arias (Mar 29 2017 at 22:03):

the summary of that discussion is

Emilio Jesús Gallego Arias (Mar 29 2017 at 22:04):

Show Match is used only by Proof General, thus before documenting it, please confirm you agree with the spec

Emilio Jesús Gallego Arias (Mar 29 2017 at 22:04):

so both @Clément Pit-Claudel and @matafou should IMO say "we agree with the current specification of Show Match, the docs can go ahead

Emilio Jesús Gallego Arias (Mar 29 2017 at 22:05):

or "we think Show Match should be modified in this particular way"

Emilio Jesús Gallego Arias (Mar 29 2017 at 22:05):

and then we follow suit

Maxime Dénès (Mar 29 2017 at 22:06):

ok thanks !

Emilio Jesús Gallego Arias (Mar 29 2017 at 23:40):

Hey @/all , what would be the best way to group bugs for a particular component ? [lets say the STM] Should I create a new component? Tags?

Emilio Jesús Gallego Arias (Mar 29 2017 at 23:41):

For instance, there are many bugs now reported in the IDE component that are actually problems in the STM

Maxime Dénès (Mar 30 2017 at 07:49):

@Emilio Jesús Gallego Arias I added an STM component

Emilio Jesús Gallego Arias (Mar 30 2017 at 08:12):

cool thanks

Maxime Dénès (Mar 30 2017 at 09:09):

@Emilio Jesús Gallego Arias you recently mentioned the ocaml room. Is there one?

Emilio Jesús Gallego Arias (Mar 30 2017 at 09:13):

Nope. BTW, it seems that gforge was down for a bit, so you'll see some travis problem related to that, rescheduling jobs.

Emilio Jesús Gallego Arias (Mar 30 2017 at 12:05):

By the way, how about informally announcing this room ? Do the rest of developers know about it?

Maxime Dénès (Mar 30 2017 at 12:35):

Not really. I think I fear is that I was already spammed quite a lot by Gitter. Some devs won't like it. I didn't even find a way to turn off all notifications!

Emilio Jesús Gallego Arias (Mar 30 2017 at 12:46):

Well, I don't see the problem, as this is opt-in. Announcing is different from requiring to join IMHO. Secondly, yeah it is like github, you can't turn notifications off if you are directly mentioned. I dunno if leaving the room disables that thou.

Emilio Jesús Gallego Arias (Mar 30 2017 at 12:48):

Again if you don't announce it, it is hard to get some feedback. I don't understand what we are afraid of here...

Emilio Jesús Gallego Arias (Mar 30 2017 at 12:48):

We seem to be too afraid sometimes I think....

Maxime Dénès (Mar 30 2017 at 13:30):

oh, I wasn't saying we shouldn't announce it

Maxime Dénès (Mar 30 2017 at 13:30):

I thought you'd do it :)

Théo Zimmermann (Mar 30 2017 at 13:47):

Apparently @Pierre-Marie Pédrot found about it too.

Théo Zimmermann (Mar 30 2017 at 13:47):

Let's just have people join one by one and once we are satisfied enough we can make an announcement.

Pierre-Marie Pédrot (Mar 30 2017 at 13:47):

@Théo Zimmermann I've been forcefully dragged into gitter because it is where the cool guys are nowadays... Sigh.

Théo Zimmermann (Mar 30 2017 at 13:48):

Are the three of us the cool guys? Nice ;-)

Théo Zimmermann (Mar 30 2017 at 13:49):

Is the wiki activated on the CEP repo or not? I can see the tab but when I click on it, I stay on the main page.

Maxime Dénès (Mar 30 2017 at 13:51):

@Pierre-Marie Pédrot You were dragged only because you wanted to, deep inside :D

Théo Zimmermann (Mar 30 2017 at 13:51):

I'd like to use this wiki for listing feature requests before one can make a real CEP.

Emilio Jesús Gallego Arias (Mar 30 2017 at 13:51):

I'll take care of it @Maxime Dénès , isn't this chat wonderful, now we can say politically incorrect things live, publicly, and without the possibility of correcting them later

Emilio Jesús Gallego Arias (Mar 30 2017 at 13:51):

@Maxime Dénès @Pierre-Marie Pédrot puns always taste better live

Théo Zimmermann (Mar 30 2017 at 13:51):

Well there is an edit function

Pierre-Marie Pédrot (Mar 30 2017 at 13:51):

@Emilio Jesús Gallego Arias Yay! That's exactly what I wanted to do.

Pierre-Marie Pédrot (Mar 30 2017 at 13:52):

I mean, right now.

Maxime Dénès (Mar 30 2017 at 13:52):

@Emilio Jesús Gallego Arias indeed, I usually say politically incorrect things on videos whose sound nobody can hear, this is way better!

Emilio Jesús Gallego Arias (Mar 30 2017 at 13:52):

We ougtha admit it, our dream has become true!

Théo Zimmermann (Mar 30 2017 at 13:52):

Maxime Dénès (Mar 30 2017 at 13:52):

@Pierre-Marie Pédrot Matej and I improved the bench script, and EConstr is being benched

Emilio Jesús Gallego Arias (Mar 30 2017 at 13:54):

EConstr is almost ready to go, right?

Pierre-Marie Pédrot (Mar 30 2017 at 13:54):

I hope so...

Emilio Jesús Gallego Arias (Mar 30 2017 at 13:55):

fantastic

Théo Zimmermann (Mar 30 2017 at 13:56):

@Emilio Jesús Gallego Arias Do you have maintainer rights on the CEP repo now?

Pierre-Marie Pédrot (Mar 30 2017 at 13:56):

My main center of attention today is not EConstr and the craziness of unification it unveiled. I am instead loathing in algorithmic and architectural despair about Nsatz.

Pierre-Marie Pédrot (Mar 30 2017 at 13:56):

@Maxime Dénès Do I have the right to waste the day rewriting this... code?

Emilio Jesús Gallego Arias (Mar 30 2017 at 13:56):

Uhhh

Maxime Dénès (Mar 30 2017 at 13:56):

@Pierre-Marie Pédrot No :)

Emilio Jesús Gallego Arias (Mar 30 2017 at 13:57):

anything ending in "z" cannot be any good

Pierre-Marie Pédrot (Mar 30 2017 at 13:57):

Come on. Little algorithmic complexity quizz:

      let lc = List.nth lci k in
      for i=0 to List.length lc - 1 do
    if not (zero (List.nth lc i))
    then utiles (i+k+1);
      done

Maxime Dénès (Mar 30 2017 at 13:57):

@Pierre-Marie Pédrot I mean, we need to merge EConstr. The early results seem to indicate some slowdown (not huge, but significant) in most devs. How about pushing the unrolling patch for EConstr.kind?

Pierre-Marie Pédrot (Mar 30 2017 at 13:58):

I'm waiting for detailed slowness report to see where things go wrong.

Maxime Dénès (Mar 30 2017 at 13:59):

Isn't this unrolling easy to implement? We could bench with it and see the numbers, don't you think?

Pierre-Marie Pédrot (Mar 30 2017 at 13:59):

@mdenes Did you use a special Travis overlay for your branch BTW? It doesn't seem to compile on my own branch.

Emilio Jesús Gallego Arias (Mar 30 2017 at 14:00):

@Théo Zimmermann no, coq/ceps is not added to group permissions

Pierre-Marie Pédrot (Mar 30 2017 at 14:00):

@Maxime Dénès Lemme write the unrolling and push it to my branch then.

Maxime Dénès (Mar 30 2017 at 14:00):

@Pierre-Marie Pédrot For mathcomp, yes. But I pushed it on my branch, didn't you merge from there?

Pierre-Marie Pédrot (Mar 30 2017 at 14:01):

Yes I did. But something does not seem to work because it still downloads the default repo.

Maxime Dénès (Mar 30 2017 at 14:01):

@Pierre-Marie Pédrot You deserve better than turning lists into arrays :)

Emilio Jesús Gallego Arias (Mar 30 2017 at 14:01):

yeah if that is for polynomials you may want some more complex stuff

Pierre-Marie Pédrot (Mar 30 2017 at 14:01):

And using arguments to actually pass something to a function rather than global variables?

Emilio Jesús Gallego Arias (Mar 30 2017 at 14:02):

arguments are overrated

Maxime Dénès (Mar 30 2017 at 14:02):

That's because you don't know about purely imperative programming

Emilio Jesús Gallego Arias (Mar 30 2017 at 14:02):

the STM manages to do everything without them

Pierre-Marie Pédrot (Mar 30 2017 at 14:02):

I mean even by keeping the same algorithmic core, there are crazy stuff going in there.

Maxime Dénès (Mar 30 2017 at 14:02):

A very common paradigm in baroque programming.

Pierre-Marie Pédrot (Mar 30 2017 at 14:03):

I'm not even able to reason on those functions. And perfing indicate really fishy hotspots.

Emilio Jesús Gallego Arias (Mar 30 2017 at 14:03):

  val define :
    ?safe_id:Stateid.t ->
    ?redefine:bool -> ?cache:Summary.marshallable ->
    ?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit

Emilio Jesús Gallego Arias (Mar 30 2017 at 14:03):

once you remove the unnecasrry optional arguments, it will be perfect

Emilio Jesús Gallego Arias (Mar 30 2017 at 14:04):

val define : (unit -> unit) -> unit

Maxime Dénès (Mar 30 2017 at 14:04):

@Pierre-Marie Pédrot I'm fine with you fixing it, but after we get the work done on EConstr and Ltac 2. Those have a bus factor of 1. My son can fix you Nsatz example.

Pierre-Marie Pédrot (Mar 30 2017 at 14:04):

This still takes a function. Where is your val foo : ref (unit -> unit) ?

Emilio Jesús Gallego Arias (Mar 30 2017 at 14:05):

That is just for convenience when doing CPS

Pierre-Marie Pédrot (Mar 30 2017 at 14:05):

Okay okay. I'm writing the EConstr stuff right now.

Emilio Jesús Gallego Arias (Mar 30 2017 at 14:05):

we must retain some elegance

Emilio Jesús Gallego Arias (Mar 30 2017 at 14:05):

purely imperative CPS

Pierre-Marie Pédrot (Mar 30 2017 at 14:05):

No more slacking around on this chat!

Emilio Jesús Gallego Arias (Mar 30 2017 at 14:05):

yeah

Emilio Jesús Gallego Arias (Mar 30 2017 at 14:05):

right!

Théo Zimmermann (Mar 30 2017 at 14:05):

Pierre-Marie Pédrot I'm fine with you fixing it, but after we get the work done on EConstr and Ltac 2. Those have a bus factor of 1. My son can fix you Nsatz example.

How old is your son?

Pierre-Marie Pédrot (Mar 30 2017 at 14:06):

Not old enough to consume alcohol not to drown into depression.

Maxime Dénès (Mar 30 2017 at 14:06):

Less than two years old, but he can reach the keyboard. That's the only required skill.

Maxime Dénès (Mar 30 2017 at 14:07):

If this chat manages to keep PMP focused on work that matters for Coq, I'll be truly impressed :D

Pierre-Marie Pédrot (Mar 30 2017 at 14:07):

I'm trying to look at the generated assembly to see what we can do.

Emilio Jesús Gallego Arias (Mar 30 2017 at 14:07):

He was born inside an INRIA audition, so he got some advantage

Emilio Jesús Gallego Arias (Mar 30 2017 at 14:08):

If this chat manages to keep PMP focused on work that matters for Coq, I'll be truly impressed

I am searching for the "send coin" plugin in the style of the finest old internet chats, so that won't be cheap for you

Théo Zimmermann (Mar 30 2017 at 14:10):

@Maxime Dénès is your notification problem when the tab in the browser is open? or have you installed the mobile app? or are you receiving e-mails?

Maxime Dénès (Mar 30 2017 at 14:11):

@Théo Zimmermann It's not a problem for me, I thought it could be for other developers, and I meant e-mails.

Théo Zimmermann (Mar 30 2017 at 14:12):

OK, because I received once an email telling me about unread messages, I clicked the "unsubscribe from all emails" button and have not received any more email since

Théo Zimmermann (Mar 30 2017 at 14:12):

but maybe it's just because people don't @ mention me enough

Maxime Dénès (Mar 30 2017 at 14:13):

I think you are right, there are actually two links. I tried only the first (notification settings).

Théo Zimmermann (Mar 30 2017 at 14:14):

and I thought that programmers were good at understanding those things :D

Maxime Dénès (Mar 30 2017 at 14:14):

To answer partially a question I asked here yesterday, there is ongoing work for gdb support in OCaml: http://mshinwell.github.io/libmonda/

Emilio Jesús Gallego Arias (Mar 30 2017 at 14:17):

Great!

Maxime Dénès (Mar 30 2017 at 14:20):

@Théo Zimmermann My IQ was getting close to 0 after spending nights and days with @Pierre-Marie Pédrot and @Matthieu Sozeau understanding that apply relies on heuristics that mutate user flags under conditions that are typically the ones you don't want, but fortunately through a testing of the conditions that is completely bogus, until EConstr fixes it...

Maxime Dénès (Mar 30 2017 at 14:23):

@Emilio Jesús Gallego Arias We seem to get a number of timeouts on fiat-crypto these days. Should we compile only part of it?

Pierre-Marie Pédrot (Mar 30 2017 at 14:23):

@Maxime Dénès If you were willing to merge my optimizations, it should probably manage to compile... (Not to mention Nsatz.)

Maxime Dénès (Mar 30 2017 at 14:24):

Ah ah! Well done :)

Maxime Dénès (Mar 30 2017 at 14:24):

Let's see. Do you have in mind some that were already benchmarked?

Pierre-Marie Pédrot (Mar 30 2017 at 14:25):

At least the array mapping in the kernel. But when pendulum is free, I'll overrun it with benchmarks.

Maxime Dénès (Mar 30 2017 at 14:27):

@Pierre-Marie Pédrot I made some local changes to the script to get EConstrto compile, because @matejkosik hasn't implemented overlays yet. So I'll undo them once EConstr is finished, before you can run other benchmarks.

Maxime Dénès (Mar 30 2017 at 14:29):

@Pierre-Marie Pédrot Also, for now it goes way faster if you give the packages in topological order. @matejkosik is working on using OPAM to compute this order automatically.

Emilio Jesús Gallego Arias (Mar 30 2017 at 14:30):

I understood the first priority was to separete into "install phase" "clean phase" "build phase" right

Emilio Jesús Gallego Arias (Mar 30 2017 at 14:30):

why does it go faster? shouldn't be .opam just cached?

Maxime Dénès (Mar 30 2017 at 14:31):

I'll let @matejkosik give more details :)

Emilio Jesús Gallego Arias (Mar 30 2017 at 14:32):

okk

Pierre-Marie Pédrot (Mar 30 2017 at 14:41):

@Maxime Dénès I've just pushed an unrolling of EConstr.kind on my econstr branch. You should rebase your branch on it.

Maxime Dénès (Mar 30 2017 at 14:42):

Is there anything in my branch which is not in yours?

Pierre-Marie Pédrot (Mar 30 2017 at 14:42):

Nope.

Pierre-Marie Pédrot (Mar 30 2017 at 14:43):

I've rebased against yours before commiting.

Maxime Dénès (Mar 30 2017 at 14:43):

So I can just bench your branch, I guess :)

Pierre-Marie Pédrot (Mar 30 2017 at 14:43):

Probably.

Maxime Dénès (Mar 30 2017 at 14:43):

I'll let the current benchmark finish, though, so that we can compare EConstr alone / EConstr with unrolling / trunk

Pierre-Marie Pédrot (Mar 30 2017 at 14:44):

I'd still like to know where things are slow by perfing and optimizing the hotspots.

Pierre-Marie Pédrot (Mar 30 2017 at 14:44):

How long do you think it will take for the current bench to end?

Maxime Dénès (Mar 30 2017 at 14:44):

@Pierre-Marie Pédrot you will probably need more detailed information than what the bench currently gives, right? If that is the case, feel free to open an issue at: https://github.com/coq/coq-bench

Maxime Dénès (Mar 30 2017 at 14:45):

Not long, it reached CompCert already

Pierre-Marie Pédrot (Mar 30 2017 at 14:45):

How many times are you benching each package?

Maxime Dénès (Mar 30 2017 at 14:45):

once only

Pierre-Marie Pédrot (Mar 30 2017 at 14:45):

And it did not finished yet? I thought it took about 7h, and you started it like today at 2:00am.

Maxime Dénès (Mar 30 2017 at 14:46):

Right, I didn't tell you about the EConstr curse.

Maxime Dénès (Mar 30 2017 at 14:46):

All national Inria services crashed last night, CI included...

Pierre-Marie Pédrot (Mar 30 2017 at 14:46):

-_-

Pierre-Marie Pédrot (Mar 30 2017 at 14:47):

Unification Pharaoh probably put a curse on this code. We've disturbed his sleep and we're going to pay for it.

Maxime Dénès (Mar 30 2017 at 14:47):

But before restarting it, I requested some improvements to make it way faster, that @matejkosik implemented. We were recompiling dependencies a quadratic number of times...

Maxime Dénès (Mar 30 2017 at 14:48):

So it should be faster now.

Pierre-Marie Pédrot (Mar 30 2017 at 14:48):

Were there a lot of dependencies? I thought everybody was still embedding what they needed (e.g. flocq)

Maxime Dénès (Mar 30 2017 at 14:52):

Mathcomp is split in many packages...

Emilio Jesús Gallego Arias (Mar 30 2017 at 14:59):

If you are curious a simple calculus show that you will lose way less time losing time now to properly implement the cache and benchmark than not doing so

Pierre-Marie Pédrot (Mar 30 2017 at 15:04):

Seriously, what kind of drug do you need to take to write this stuff:

let lci = ref lci in
List.iter (fun x -> lci := List.tl (!lci)) lp0;
!lci

Emilio Jesús Gallego Arias (Mar 30 2017 at 15:06):

would you blame that on the type of List.tl ?

Emilio Jesús Gallego Arias (Mar 30 2017 at 15:06):

Emilio Jesús Gallego Arias (Mar 30 2017 at 15:07):

it is beautiful, amazing

Pierre-Marie Pédrot (Mar 30 2017 at 15:08):

Alternative explanation: Nsatz has been processed by a highly cunning obfuscator able to compile elegant functional constructions to imperative ML with higher-order functions. This has to be it.

Emilio Jesús Gallego Arias (Mar 30 2017 at 15:09):

maybe https://erowid.org/chemicals/pcp/ ?

Emilio Jesús Gallego Arias (Mar 30 2017 at 15:10):

Yeah had they used the unit -> unit way it would have been way more elegant

Maxime Dénès (Mar 30 2017 at 15:11):

@Emilio Jesús Gallego Arias who were you talking to about the cache?

Emilio Jesús Gallego Arias (Mar 30 2017 at 15:13):

to @jenkins folks

Emilio Jesús Gallego Arias (Mar 30 2017 at 15:13):

whoever they are

Maxime Dénès (Mar 30 2017 at 15:24):

@Pierre-Marie Pédrot it seems that it will take some work to convince people that optimizations may be necessary

Emilio Jesús Gallego Arias (Mar 30 2017 at 15:45):

well @silene has a point with the comment

Emilio Jesús Gallego Arias (Mar 30 2017 at 15:45):

maybe you should just folks use flambda

Emilio Jesús Gallego Arias (Mar 30 2017 at 15:45):

and let non flambda users pay the cost

Pierre-Marie Pédrot (Mar 30 2017 at 15:46):

Flambda cannot make wonders I'm afraid.

Emilio Jesús Gallego Arias (Mar 30 2017 at 15:46):

too many of these optimizations are becoming necessary, so something is off

Pierre-Marie Pédrot (Mar 30 2017 at 15:46):

Not quite. The kernel needs to be fine-tuned, as well as the tactic engine.

Emilio Jesús Gallego Arias (Mar 30 2017 at 15:47):

It is been a while since I tried, but well, it looks like in this case it would work thou it may have a hard time with the opaqueness here

Emilio Jesús Gallego Arias (Mar 30 2017 at 15:47):

well, the evar_map thing is fundamentally off, in the sense that evar maps are inherently turtle-slow

Pierre-Marie Pédrot (Mar 30 2017 at 15:48):

It's actually not that much of a hot-spot when you look at it. Obviously, it may become so after the merge of EConstr.

Emilio Jesús Gallego Arias (Mar 30 2017 at 15:48):

they are turtle-slow, as @gares pointed out usually one order of magnitude, so yeah, I wonder how to optimize an intrinsically slow approach; it may be a hard battle to win in the end

Emilio Jesús Gallego Arias (Mar 30 2017 at 15:49):

but yeah we'll have to live with stuff like that for now I'm afraid

Théo Zimmermann (Mar 30 2017 at 17:11):

I'd like to create a wiki page to gather feature requests about typeclasses eauto, in order to have material so that someone, someday can make a CEP out of it. Do you agree it would make sense to do that on the GitHub wiki of the CEP repository? If yes, can someone like @Maxime Dénès activate the wiki pages of this repo?

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:34):

Why not on the main coq page?

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:34):

I think we could just have the wiki there

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:34):

I think given the number of people it makes sense to have everything in the same place

Théo Zimmermann (Mar 30 2017 at 17:34):

Two reasons:

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:35):

¡Hola @Jason Gross !

Théo Zimmermann (Mar 30 2017 at 17:35):

1) this is specifically linked to CEPs

Jason Gross (Mar 30 2017 at 17:35):

Hi!

Théo Zimmermann (Mar 30 2017 at 17:35):

Jason Gross (Mar 30 2017 at 17:35):

(I'm mostly just observing/reading now; I don't have anything to say at the moment)

Théo Zimmermann (Mar 30 2017 at 17:36):

2) If we need to have everything in the same place, there is already Cocorico so I can just create a page there. But the pb is, I don't like Cocorico

Théo Zimmermann (Mar 30 2017 at 17:36):

Just the fact that you cannot double click on a page scares me away

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:38):

2) I agree; however 1) I am not so sure

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:38):

I can't see where the CEP process is going

Théo Zimmermann (Mar 30 2017 at 17:38):

In fact, if this is a successful experience, I would then add a link from the README to the wiki

Théo Zimmermann (Mar 30 2017 at 17:38):

Well, I like the CEP process a lot.

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:38):

So far what are the results?

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:38):

How many CEPs turned into something real?

Théo Zimmermann (Mar 30 2017 at 17:38):

I think it helps take decisions which were really thought through

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:39):

such as?

Théo Zimmermann (Mar 30 2017 at 17:39):

Several, let me count

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:39):

do you have an example

Théo Zimmermann (Mar 30 2017 at 17:41):

numeral notation has now a new PR, opam metadata I think it was implemented somehow, ltac2 is being implemented, your stuff on printing was merged (at least the first part of it) and econstr is going to get merged

Théo Zimmermann (Mar 30 2017 at 17:41):

Plus, I think the new CEP process (as advocated by @silene and @gares) is better

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:42):

Well for my stuff on printing, the CEP didn't really provide me not a single comment. The PR a few more. That is my point, given what is going on, we could just have wiki pages in coq/coq + the PRs

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:42):

associated at each CEP

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:42):

and then it is better as we can migrate things easilier to documentation

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:42):

etc...

Théo Zimmermann (Mar 30 2017 at 17:43):

How so?

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:43):

Same repository

Théo Zimmermann (Mar 30 2017 at 17:43):

And?

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:43):

vs ceps-wiki / coq-wiki

Théo Zimmermann (Mar 30 2017 at 17:43):

But doc is not in a wiki anyways

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:43):

Oh some of it is

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:43):

in Cocoriko

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:43):

that hopefully is migrated to coq / coq

Théo Zimmermann (Mar 30 2017 at 17:44):

Yes, well it's mostly outdated doc

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:44):

anyways a good proof of the overhead

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:44):

is that actually we cannot get CEP merged

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:44):

or touch anything in the coq-ceps

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:44):

because some permission problem

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:44):

so indeed, there is an overhead of having so many wikis

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:44):

IMHO

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:44):

if we have a wiki

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:44):

we should have a single one

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:44):

for Coq

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:45):

that means

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:45):

cocorico is out if we add another wiki

Théo Zimmermann (Mar 30 2017 at 17:45):

I don't like wikis. At least not for any purpose.

Théo Zimmermann (Mar 30 2017 at 17:45):

I like Wikipedia but it's much more than just a wiki

Maxime Dénès (Mar 30 2017 at 17:45):

@Emilio Jesús Gallego Arias Could you announce the gitter experiment? If some users are aware of its existence, it would be better to tell developers ;)

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:46):

@maxime today I have a very complicated day so I may not be able to do it

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:46):

@Maxime Dénès

Emilio Jesús Gallego Arias (Mar 30 2017 at 17:46):

I mean

Théo Zimmermann (Mar 30 2017 at 17:46):

I want to test the GitHub wiki before arguing to move to the GitHub wiki. Do you see my point?

Théo Zimmermann (Mar 30 2017 at 17:51):

Anyways, given your reluctance to open a wiki on the CEP repo, I think I will just create a Cocorico page.

Emilio Jesús Gallego Arias (Mar 30 2017 at 18:00):

Oh well, I don't have myself rights to modify the CEP repo, so all that I can offer is to open the wiki in the coq repository if others agree, you can also open the wiki in your own cep clone. I am not reluctant to the wiki, but indeed I would appreciate having a single wiki for Coq; of course that is just my opinion.

Emilio Jesús Gallego Arias (Mar 30 2017 at 18:00):

I _really_ get confused with several wikis, etc...

Maxime Dénès (Mar 30 2017 at 18:01):

I'm fine with anything, but we indeed need some coordination.

Maxime Dénès (Mar 30 2017 at 18:02):

I would be in favor of not maintaining our own wiki platform (like Cocorico), as long as the platform we choose has APIs that can make a transfer and backups easy

Emilio Jesús Gallego Arias (Mar 30 2017 at 18:02):

Githubs wikis are just git repositories with markdown.

Emilio Jesús Gallego Arias (Mar 30 2017 at 18:02):

so that is not _too_ bad

Maxime Dénès (Mar 30 2017 at 18:03):

@Pierre-Marie Pédrot the bench of you branch failed with an old error. Are you sure you merged all commits from my pr379 branch?

Pierre-Marie Pédrot (Mar 30 2017 at 18:03):

Yep, you can check on gitk that I'm just above your commit.

Pierre-Marie Pédrot (Mar 30 2017 at 18:03):

There is trickery in the travis overlay to check whether we're on your pr379 branch or not

Pierre-Marie Pédrot (Mar 30 2017 at 18:04):

That way the right version of compcert is downloaded. I've mentionned that somewhere before in this thread.

Maxime Dénès (Mar 30 2017 at 18:04):

But jenkins doesn't use overlays AFAIK

Pierre-Marie Pédrot (Mar 30 2017 at 18:04):

Right, so how is compcert supposed to compile properly then?

Maxime Dénès (Mar 30 2017 at 18:05):

What fix does CompCert need for EConstr ?!

Pierre-Marie Pédrot (Mar 30 2017 at 18:05):

I mean mathcomp, sorry.

Maxime Dénès (Mar 30 2017 at 18:06):

I hacked the script run by jenkins for that, but it doesn't rely on the branch name so I'm confused

Maxime Dénès (Mar 30 2017 at 18:06):

I'll investigate

Pierre-Marie Pédrot (Mar 30 2017 at 18:07):

Wait, hasn't the error nothing to do with that? It seems Coq does not even compile.

Maxime Dénès (Mar 30 2017 at 18:08):

Indeed, and that's an error we used to have with old Coq versions on recent OCaml

Maxime Dénès (Mar 30 2017 at 18:37):

@Pierre-Marie Pédrot I looked at it, but I don't understand what is going on in this script.

Maxime Dénès (Mar 30 2017 at 18:50):

oh fuck I know why

Maxime Dénès (Mar 30 2017 at 18:50):

it takes the trunk from your repo, @Pierre-Marie Pédrot

Maxime Dénès (Mar 30 2017 at 18:53):

@Pierre-Marie Pédrot can you pull the latest trunk from the main repo and push it back to your repo? I'll relaunch the build

Maxime Dénès (Mar 30 2017 at 18:53):

It is amazing how good we are at wasting each other's time in this community...

Pierre-Marie Pédrot (Mar 30 2017 at 19:07):

There you go...

Maxime Dénès (Mar 30 2017 at 19:33):

@Pierre-Marie Pédrot Ok, this time the bench really started.

Théo Zimmermann (Mar 30 2017 at 19:37):

Cocorico is so frustrating! So many outdated pages. Immutable pages like the front page and this one https://coq.inria.fr/cocorico/CoqDevelopment/Public which I'd like to update.

Théo Zimmermann (Mar 30 2017 at 19:38):

If we ever move to a new wiki, I think we should not copy-paste the existing pages. Better to just mark the current wiki as deprecated as it is done here https://nixos.org/wiki/Main_Page and start fresh.

Emilio Jesús Gallego Arias (Mar 31 2017 at 09:04):

Well, it seems the loop unrolling barely had any effect (well within a statistic error margin)

Emilio Jesús Gallego Arias (Mar 31 2017 at 09:05):

So indeed, how can we help to see where time is spend, would having a line to line time diff help here?

Emilio Jesús Gallego Arias (Mar 31 2017 at 09:06):

I think Jason has some tools for that, but we can cook our own

Emilio Jesús Gallego Arias (Mar 31 2017 at 09:07):

In particular for hott, right?

Emilio Jesús Gallego Arias (Mar 31 2017 at 09:07):

Was it make timing

Emilio Jesús Gallego Arias (Mar 31 2017 at 09:07):

@Jason Gross ?

Maxime Dénès (Mar 31 2017 at 09:35):

Yeah we need something more detailed.

Emilio Jesús Gallego Arias (Mar 31 2017 at 09:39):

Unfortunately HoTT stuff is geared towards tracking time regressions in the library itself, again it tries to guess commits and stuff like that

Emilio Jesús Gallego Arias (Mar 31 2017 at 11:07):

So hey folks, that's my updated tree for flambda https://github.com/ejgallego/coq/tree/flambda

Emilio Jesús Gallego Arias (Mar 31 2017 at 11:09):

It is WIP as it needs some tweaks, namely:

must add an option to configure so it can parse the flags instead of hardcoding them.
should tweak coqmktop as not to require hardcoded flags recognition. Honestly the whole of coqmktop should go away, but that's another history.

Emilio Jesús Gallego Arias (Mar 31 2017 at 12:44):

¡Hola @Matej Košík! Comment vas tu ?

Pierre-Marie Pédrot (Mar 31 2017 at 12:44):

I didn't know romance languages were allowed here.

Emilio Jesús Gallego Arias (Mar 31 2017 at 12:47):

I love romance

Maxime Dénès (Mar 31 2017 at 14:28):

@Pierre-Marie Pédrot whas is universe normalization? Is it the same as minimization?

Maxime Dénès (Mar 31 2017 at 14:28):

what is*

Pierre-Marie Pédrot (Mar 31 2017 at 14:29):

No, it is the fact that universes have a value depending on the current universe unification state (as in UState).

Pierre-Marie Pédrot (Mar 31 2017 at 14:29):

If you get a variable, it can be instantiated later on by some other expression.

Maxime Dénès (Mar 31 2017 at 14:33):

ah! Like a local universe can become a global one?

Pierre-Marie Pédrot (Mar 31 2017 at 14:33):

Yep.

Maxime Dénès (Mar 31 2017 at 14:33):

So we don't have the same strategy for universes and terms? I.e. evar normalization vs univ normalization?

Pierre-Marie Pédrot (Mar 31 2017 at 14:34):

Universe-operating functions ought to be insensitive as well (cough cough).

Maxime Dénès (Mar 31 2017 at 14:34):

Oh my god.

Pierre-Marie Pédrot (Mar 31 2017 at 14:34):

Indeed.

Pierre-Marie Pédrot (Mar 31 2017 at 14:35):

Luckily, the attack surface is way smaller than with evars.

Pierre-Marie Pédrot (Mar 31 2017 at 14:35):

Although one should be afraid of Type u being unified to Set / Prop.

Matej Košík (Gitter import) (Mar 31 2017 at 14:35):

@Emilio Jesús Gallego Arias Parfaitement! Et toi? Qu'est-ce que tu fait maintenant? (quand tu n'ouvers pas des issues?)

Maxime Dénès (Mar 31 2017 at 14:36):

@Matej Košík If you have further questions like the git clone one, don't hesitate to ask here, in case I'm not available, you'll get answers faster

Pierre-Marie Pédrot (Mar 31 2017 at 14:36):

Can I spam pendulum with benchmarks btw?

Matej Košík (Gitter import) (Mar 31 2017 at 14:36):

Ok.

Matej Košík (Gitter import) (Mar 31 2017 at 14:36):

Well, I am not sure what is the protocol?\

Matej Košík (Gitter import) (Mar 31 2017 at 14:36):

Do we want to run the benchmarks always via Jenkins?

Matej Košík (Gitter import) (Mar 31 2017 at 14:37):

Is hat sufficient?

Pierre-Marie Pédrot (Mar 31 2017 at 14:37):

I don't know, I'm happy with the ci interface.

Matej Košík (Gitter import) (Mar 31 2017 at 14:37):

If yes, then one can see quite easily whether something is being benchmarked or not. No?

Maxime Dénès (Mar 31 2017 at 14:37):

Yes we always want to run benchmarks via Jenkins, because it enforces to have only one running job.

Maxime Dénès (Mar 31 2017 at 14:38):

But I think what PMP is really asking is if your script has stabilized

Pierre-Marie Pédrot (Mar 31 2017 at 14:38):

Yes, I meant that.

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:39):

@Matej Košík je suis emmerdé avec l'ANR

Matej Košík (Gitter import) (Mar 31 2017 at 14:40):

@Maxime Dénès @Pierre-Marie Pédrot Please try it. I am still testing it (with the most simple cases progressively to the more realistic ones) but I haven't finished. But so far I haven't found a problem.

Maxime Dénès (Mar 31 2017 at 14:40):

Have you pulled the latest version?

Matej Košík (Gitter import) (Mar 31 2017 at 14:40):

The script should behave consistently with the open/closed status of the issues.

Matej Košík (Gitter import) (Mar 31 2017 at 14:41):

(on github)

Maxime Dénès (Mar 31 2017 at 14:41):

For other people, you mean here: https://github.com/coq/coq-bench/issues

Pierre-Marie Pédrot (Mar 31 2017 at 14:41):

Universe rocket launched on pendulum. Let's see what happens.

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:41):

@Maxime Dénès @Pierre-Marie Pédrot I know I am a bit annoying with that thing so I won't mention it again, but don't you think that the naming choices of "evar normalization" / "evar insensitive" are quite misleading? In particular, I think they seriously downplay the issue and kind of legitimate "evar sensitivity"

Matej Košík (Gitter import) (Mar 31 2017 at 14:42):

@Maxime Dénès I have pushed it but I haven't pulled it on pendulum. When inconvenience is that there are local modifications (sort of overlay) which is something missing and needs to be supported as well officially.

Matej Košík (Gitter import) (Mar 31 2017 at 14:42):

@Pierre-Marie Pédrot +1

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:43):

@Matej Košík for sure we will want to benchmark with flambda, this implies a) building coq configured with a particular set of flags depending on the benchmark -flambda-flags "-03 -inline" etc... and b) using a particular ocaml switch

Pierre-Marie Pédrot (Mar 31 2017 at 14:43):

@Emilio Jesús Gallego Arias Well, what do you propose?

Maxime Dénès (Mar 31 2017 at 14:43):

@Matej Košík Yeah but for now, there is none, right? Anyway you should always keep the repo and pendulum in sync, otherwise we get no change of understanding what the script does.

Maxime Dénès (Mar 31 2017 at 14:43):

@Emilio Jesús Gallego Arias I agree with you, so what should we call it? "evar fuck up"?

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:43):

@Pierre-Marie Pédrot "dereference fault"?

Maxime Dénès (Mar 31 2017 at 14:43):

"existential delirium"?

Matej Košík (Gitter import) (Mar 31 2017 at 14:44):

@Emilio Jesús Gallego Arias Can you please open the issue? (so that we don't forget). I'll check out what you mean.

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:44):

"functions not properly dereferencing evars?

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:45):

@Matej Košík ok, I will do later on, just keep in mind that the scripts need to be able to configure coq with specific sets of flags

Pierre-Marie Pédrot (Mar 31 2017 at 14:45):

I like existential delirium.

Pierre-Marie Pédrot (Mar 31 2017 at 14:45):

Existential Delirium in the Evar Hell

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:45):

_fucked existential delirium fault_

Pierre-Marie Pédrot (Mar 31 2017 at 14:45):

looks like a novel title

Pierre-Marie Pédrot (Mar 31 2017 at 14:46):

We can go the medical way otherwise

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:46):

Existential Delirium in the Dereferencing Hell?

Pierre-Marie Pédrot (Mar 31 2017 at 14:46):

What about evarititis

Maxime Dénès (Mar 31 2017 at 14:46):

I hope it's not the title of the novel you write when we finally solve the last EConstr bug, in 20 years...

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:46):

evaritis is good

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:46):

but Coq will still suffer from evarititis even after your PR

Pierre-Marie Pédrot (Mar 31 2017 at 14:46):

It should go curing itself with the time

Matej Košík (Gitter import) (Mar 31 2017 at 14:47):

@Emilio Jesús Gallego Arias Bon chance!

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:47):

@Matej Košík so it is better if we build them with that in mind from the start

Maxime Dénès (Mar 31 2017 at 14:47):

Yeah, we need an evarititis cure group

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:47):

@Matej Košík merci

Pierre-Marie Pédrot (Mar 31 2017 at 14:47):

Did I already yelled enough at the world about how fucked up is Nsatz?

Pierre-Marie Pédrot (Mar 31 2017 at 14:47):

I've been rewriting it for the whole day. And yesterday also.

Maxime Dénès (Mar 31 2017 at 14:47):

Yes, but you should yell at the right person.

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:47):

Not enough I'm afraid

Pierre-Marie Pédrot (Mar 31 2017 at 14:47):

That's just beyond words.

Pierre-Marie Pédrot (Mar 31 2017 at 14:47):

I really need a therapy.

Maxime Dénès (Mar 31 2017 at 14:47):

https://coq.inria.fr/cocorico/CoqDevelopment/Maintainers

Maxime Dénès (Mar 31 2017 at 14:48):

Laurent Théry volunteered to maintain it, so can you send him pointers on the things you find that need fixing?

Pierre-Marie Pédrot (Mar 31 2017 at 14:48):

Nah, it'll be faster to fix it myself

Pierre-Marie Pédrot (Mar 31 2017 at 14:48):

I'm already done actually

Maxime Dénès (Mar 31 2017 at 14:48):

Pierre-Marie Pédrot (Mar 31 2017 at 14:49):

but by the god of specification

Pierre-Marie Pédrot (Mar 31 2017 at 14:49):

If I had to grade this as a student work, it wouldn't pass

Maxime Dénès (Mar 31 2017 at 14:49):

But we tend to proceed like this too much, and not get the maintainers involved.

Maxime Dénès (Mar 31 2017 at 14:49):

At least make it a PR, so that he can see it.

Pierre-Marie Pédrot (Mar 31 2017 at 14:49):

How the hell did this get included in the repo?

Pierre-Marie Pédrot (Mar 31 2017 at 14:49):

Yes, I'm going to do a PR don't worry

Maxime Dénès (Mar 31 2017 at 14:49):

Inclusion of such low-quality code is the first thing we fixed.

Pierre-Marie Pédrot (Mar 31 2017 at 14:49):

but the code is so fucked up that expliciting the invariants seem like 3rd-type encounter

Maxime Dénès (Mar 31 2017 at 14:50):

Basically we recently reduced the problem to a finite one...

Matej Košík (Gitter import) (Mar 31 2017 at 14:51):

@Pierre-Marie Pédrot While your benchmarking job does not waste too much time, can we:

stop it
pull on pendulum from origin
restart it?
Because yesterday I've fixed a but that is causes benchmarking failures for number_of_terations > 1.

Maxime Dénès (Mar 31 2017 at 14:51):

That should make you feel good

Pierre-Marie Pédrot (Mar 31 2017 at 14:51):

By construction it has always be finite, come on. What you mean is that there is an eventual bound.

Pierre-Marie Pédrot (Mar 31 2017 at 14:51):

@Matej Košík OK

Pierre-Marie Pédrot (Mar 31 2017 at 14:51):

@Matej Košík Can you relauch it when you're done?

Matej Košík (Gitter import) (Mar 31 2017 at 14:51):

Ok. I'll do that.

Pierre-Marie Pédrot (Mar 31 2017 at 14:51):

thx

Maxime Dénès (Mar 31 2017 at 14:52):

@Pierre-Marie Pédrot broken code was integrated faster than cleanups, that's what I call infinite.

Maxime Dénès (Mar 31 2017 at 14:52):

You could think it was countable though, but I have doubts :)

Pierre-Marie Pédrot (Mar 31 2017 at 14:53):

I don't know Loic Pottier personally, but I'm wondering from which programming background he came. @Maxime Dénès you probably have more info about this.

Maxime Dénès (Mar 31 2017 at 14:53):

Oh by the way, what is the real answer to #526?

Pierre-Marie Pédrot (Mar 31 2017 at 14:54):

Deprecate Funind?

Pierre-Marie Pédrot (Mar 31 2017 at 14:54):

The argument of branch sharing does not make sense.

Maxime Dénès (Mar 31 2017 at 14:54):

That's not what I meant. Imagine you had to write funind today. What is the proper datatype to work on?

Pierre-Marie Pédrot (Mar 31 2017 at 14:54):

You can always check whether a constr pattern-matching is indeed coming from a wildcard, Detypign does that

Pierre-Marie Pédrot (Mar 31 2017 at 14:54):

constr

Pierre-Marie Pédrot (Mar 31 2017 at 14:55):

Obviously constr. That's the only thing that has a canonical normal form.

Maxime Dénès (Mar 31 2017 at 14:55):

And even trickier, how does a plugin author make an informed choice?

Pierre-Marie Pédrot (Mar 31 2017 at 14:55):

Meh.

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:55):

@Pierre-Marie Pédrot do you mean that glob_constr is redudant?

Pierre-Marie Pédrot (Mar 31 2017 at 14:55):

No, but it is an internal structure that you should not manipulate.

Pierre-Marie Pédrot (Mar 31 2017 at 14:56):

(Apart from producing it, storing it and pretyping it obviously.)

Maxime Dénès (Mar 31 2017 at 14:56):

Honestly, I would not be sure what datatype to use. So I don't see how people more external to the team would guess it.

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:56):

Cool, can we please add that to glob_term.mli ?? And move it away from intf

Maxime Dénès (Mar 31 2017 at 14:57):

Yeah... "On pousse mémé dans les orties"...

Pierre-Marie Pédrot (Mar 31 2017 at 14:57):

Now that I'm thinking about it, is gitter indexed by Google? So that people can find back the info...

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:57):

In fact, I don't see a reason why we shouldn't just get rid of glob_constr

Pierre-Marie Pédrot (Mar 31 2017 at 14:57):

No.

Pierre-Marie Pédrot (Mar 31 2017 at 14:57):

We need glob_constr, because that is the stable representation of data for storing.

Maxime Dénès (Mar 31 2017 at 14:57):

You should answer #526.

Maxime Dénès (Mar 31 2017 at 14:58):

It would be a start, to communicate.

Pierre-Marie Pédrot (Mar 31 2017 at 14:58):

It has all names resolved, which is important.

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:58):

the stable representation of data for storing

sorry, storing what?

Pierre-Marie Pédrot (Mar 31 2017 at 14:58):

Glob_constr

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:58):

implicits arguments are better done in the syntax tree

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:58):

notations likewise

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:58):

in fact it is much better

Pierre-Marie Pédrot (Mar 31 2017 at 14:58):

For instance when you have notations or ltac containing terms

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:58):

so that leaves us with name resolution

Pierre-Marie Pédrot (Mar 31 2017 at 14:58):

the natural type you store is glob_constr

Maxime Dénès (Mar 31 2017 at 14:58):

But you can't complain or be surprised if people use Glob_constr which is in the interface folder instead of Constr which is not.

Matej Košík (Gitter import) (Mar 31 2017 at 14:59):

@Pierre-Marie Pédrot Done.

Pierre-Marie Pédrot (Mar 31 2017 at 14:59):

Well that's not any people.

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:59):

well you could store constrexpr

Pierre-Marie Pédrot (Mar 31 2017 at 14:59):

I mean they are somehow close to the dev team.

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:59):

notations I'm pretty sure

Pierre-Marie Pédrot (Mar 31 2017 at 14:59):

@Emilio Jesús Gallego Arias but you need names to be resolved

Emilio Jesús Gallego Arias (Mar 31 2017 at 14:59):

things work much better if you resolved them over constrexpr

Maxime Dénès (Mar 31 2017 at 14:59):

WDYM? I'm pretty sure if I was new to Coq, I'd pick something in intf. Everything else would look internal to me.

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:00):

and ditto for implicits arguments, the explicit application is there

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:00):

IDES would have a great time

Pierre-Marie Pédrot (Mar 31 2017 at 15:00):

But that's not for ide

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:00):

and they could get the diff over the syntax tree, which is what it is fed to the printer

Pierre-Marie Pédrot (Mar 31 2017 at 15:00):

glob_constr is like the stablest representation of kernel constr which is invariant by things like evars, universes and the like.

Pierre-Marie Pédrot (Mar 31 2017 at 15:01):

It is like a compiled form of syntax.

Pierre-Marie Pédrot (Mar 31 2017 at 15:01):

bytecode if you want

Pierre-Marie Pédrot (Mar 31 2017 at 15:01):

while constr is really the execution trace

Pierre-Marie Pédrot (Mar 31 2017 at 15:01):

and constr_expr is raw syntax

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:01):

IMHO not worth the cost, apart that from actually both implicits and notations are resolved at the wrong level

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:01):

yeah I don't see the advantage of that

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:02):

other than creating a bit of chaos in the codebase

Pierre-Marie Pédrot (Mar 31 2017 at 15:02):

Well if we had absolute names in constr_expr that could be used instead maybe

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:03):

I think a good proof that this representation has a bad overhead/benefit ratio, is that we could remove it in a few days of work

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:03):

and I'll bet it would actually clean up things a lot

Pierre-Marie Pédrot (Mar 31 2017 at 15:03):

Don't forget the mighty funind plugin!

Pierre-Marie Pédrot (Mar 31 2017 at 15:03):

I wish you luck to port that one

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:03):

in fact if you have a look to the code

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:03):

it is barely used

Maxime Dénès (Mar 31 2017 at 15:04):

You mean Function is barely used?

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:04):

I mean glob_constr

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:04):

in fact PM is right, the main user is funind

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:05):

so indeed, funind either wants to work

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:05):

with constrexpr

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:05):

or with constr

Pierre-Marie Pédrot (Mar 31 2017 at 15:05):

You still need to extend constrexpr a bit to replace glob_constr

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:05):

not with glob_constr

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:05):

right?

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:05):

only for references?

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:05):

the rest is there

Maxime Dénès (Mar 31 2017 at 15:05):

IMHO the highest priority would be to give people a chance to write correct code

Pierre-Marie Pédrot (Mar 31 2017 at 15:05):

beware of the scope for tactic interpretation also

Pierre-Marie Pédrot (Mar 31 2017 at 15:06):

and probably for arguments also

Pierre-Marie Pédrot (Mar 31 2017 at 15:06):

so in the end you end up rewriting glob_constr i think

Maxime Dénès (Mar 31 2017 at 15:06):

At least documenting what datatype they are supposed to use, and have intf reflect that.

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:11):

for tactic interpreation I have no clue, but for the rest I dunno. The evidence is there, it is barely used. In fact, it is not hard to come with uses for notations or implicits where you would like the elaboration to happen in the pretyper (not that I am advocaing such cases)

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:11):

anyways just a comment

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:11):

IMHO the issue is settles

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:11):

settled

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:11):

as it is really an internal thing

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:11):

and plugins should be forbidden to use glob_constr which I fully support

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:12):

so then if we want to optimize the internal notation handling, etc... we could see how we do

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:12):

IMHO now we have a lot of overhead and I fail to see the advantages

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:13):

in the sense

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:13):

it would be just adding 3 cases to the pretyper

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:13):

one for notations => call the notation compiler

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:13):

one for reference => call the reference solved

Maxime Dénès (Mar 31 2017 at 15:13):

I fee like I'm repeating myself, but before forbidding, we should at least document it, right?

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:13):

one for impargs => call the impargs inserted

Emilio Jesús Gallego Arias (Mar 31 2017 at 15:13):

inserter

Maxime Dénès (Mar 31 2017 at 15:17):

@Pierre-Marie Pédrot Coming back to EConstr, one thing I still don't fully understand is why EConstr changed the universe normalization strategy.

Pierre-Marie Pédrot (Mar 31 2017 at 15:17):

What do you mean?

Pierre-Marie Pédrot (Mar 31 2017 at 15:17):

It does what it should do.

Pierre-Marie Pédrot (Mar 31 2017 at 15:17):

nf_evar was doing that as well

Maxime Dénès (Mar 31 2017 at 15:24):

you mean whd_evar?

Pierre-Marie Pédrot (Mar 31 2017 at 15:25):

yep, that's the same

Maxime Dénès (Mar 31 2017 at 15:28):

Ah ok, I see what you mean now, I think. The proper fix would be that EConstr contains "non-normalized" universes. But of course, you go through a view that normalizes when actually needed, like for EConstr.

Pierre-Marie Pédrot (Mar 31 2017 at 15:28):

Exactly.

Pierre-Marie Pédrot (Mar 31 2017 at 15:28):

We could probably even be more intelligent on this one and use persistent data structures to save us from repeated normalizaton

Pierre-Marie Pédrot (Mar 31 2017 at 15:29):

There would not be such things as 'Unsafe.to_univ'

Maxime Dénès (Mar 31 2017 at 15:29):

You mean it would be more helpful than for terms?

Pierre-Marie Pédrot (Mar 31 2017 at 15:29):

It would be helpful for terms as well actually.

Pierre-Marie Pédrot (Mar 31 2017 at 15:29):

We would probably save a lot of indirections.

Pierre-Marie Pédrot (Mar 31 2017 at 15:30):

The problem is that you can't do that as long as there is a function Unsafe.to_constr which needs to be fast.

Maxime Dénès (Mar 31 2017 at 15:30):

Yeah, so let's go step by step.

Maxime Dénès (Mar 31 2017 at 15:30):

What we need is to get all EConstr overhead below 2% I'd say. Ideally without the loop unrolling.

Maxime Dénès (Mar 31 2017 at 15:30):

(and then merge)

Pierre-Marie Pédrot (Mar 31 2017 at 15:31):

Right.

Pierre-Marie Pédrot (Mar 31 2017 at 15:31):

What are the developments I should be looking at?

Maxime Dénès (Mar 31 2017 at 15:31):

I'd say we should start with the highest overheads, because fixing them may make the other ones fall into the acceptable margin.

Pierre-Marie Pédrot (Mar 31 2017 at 15:32):

HoTT is a special case, so we should not care too much at first.

Maxime Dénès (Mar 31 2017 at 15:32):

So we should start with HoTT. Verify your conjecture on universe normalization.

Pierre-Marie Pédrot (Mar 31 2017 at 15:32):

\o/

Pierre-Marie Pédrot (Mar 31 2017 at 15:32):

Alternative facts FTW.

Pierre-Marie Pédrot (Mar 31 2017 at 15:32):

OK so what should I do?

Maxime Dénès (Mar 31 2017 at 15:33):

Ok, maybe, but couldn't universe normalization impact developments that don't use polymorphism?

Pierre-Marie Pédrot (Mar 31 2017 at 15:33):

May I extend the Constr.view term to account for universes as well?

Pierre-Marie Pédrot (Mar 31 2017 at 15:33):

Well, it does change the behaviour of Type-casing.

Pierre-Marie Pédrot (Mar 31 2017 at 15:34):

The resulting view function is also going to be much more efficient once inlined I think.

Pierre-Marie Pédrot (Mar 31 2017 at 15:34):

There would be only two cases which are not identity : Evar and App.

Pierre-Marie Pédrot (Mar 31 2017 at 15:34):

Mhhh. Now that I'm thinking about it...

Maxime Dénès (Mar 31 2017 at 15:34):

So maybe the best first step is to take the slowest file in HoTT and coq-mathcomp-character and perf universe normalization.

Pierre-Marie Pédrot (Mar 31 2017 at 15:34):

There is a bug in EConstr.kind actually

Maxime Dénès (Mar 31 2017 at 15:35):

What is App doing?

Pierre-Marie Pédrot (Mar 31 2017 at 15:35):

You need to be stable by the fact that there are no two consecutive App node.

Pierre-Marie Pédrot (Mar 31 2017 at 15:35):

I'm realizing I forgot another case of smart constructors : Cast.

Maxime Dénès (Mar 31 2017 at 15:35):

Ah ah!

Pierre-Marie Pédrot (Mar 31 2017 at 15:36):

We ensure that there aren't two consecutive casts in Constr but not in EConstr.

Pierre-Marie Pédrot (Mar 31 2017 at 15:36):

I'm not sure how much this affects the semantics of Coq, seeing how casts are completely bugged anyway.

Maxime Dénès (Mar 31 2017 at 15:36):

Is the bug introduced only by your last commit?

Pierre-Marie Pédrot (Mar 31 2017 at 15:36):

No, it was there before.

Maxime Dénès (Mar 31 2017 at 15:37):

What does the Cast smart constructor do for two different kinds of Cast?

Pierre-Marie Pédrot (Mar 31 2017 at 15:37):

Eh...

Pierre-Marie Pédrot (Mar 31 2017 at 15:37):

Who knows?

Maxime Dénès (Mar 31 2017 at 15:37):

Well, if we end up removing a vm_cast somewhere...

Maxime Dénès (Mar 31 2017 at 15:38):

So how about the following plan:

Maxime Dénès (Mar 31 2017 at 15:38):

Revert the loop unrolling
Fix the Cast bug
Understand what are the slowest files in HoTT and the character theory.
Perf the universe normalization on those two files.

Pierre-Marie Pédrot (Mar 31 2017 at 15:38):

let mkCast (t1,k2,t2) =
  match t1 with
  | Cast (c,k1, _) when (k1 == VMcast || k1 == NATIVEcast) && k1 == k2 -> Cast (c,k1,t2)
  | _ -> Cast (t1,k2,t2)

Pierre-Marie Pédrot (Mar 31 2017 at 15:39):

Very strange invariant.

Pierre-Marie Pédrot (Mar 31 2017 at 15:40):

What the hell is that supposed to mean?

Maxime Dénès (Mar 31 2017 at 15:41):

The treatment of Cast should be rewritten fully.

Pierre-Marie Pédrot (Mar 31 2017 at 15:41):

So? What do we ensure for EConstr casts?

Pierre-Marie Pédrot (Mar 31 2017 at 15:41):

Same as kernel?

Maxime Dénès (Mar 31 2017 at 15:41):

Yep, at least that would not introduce a new question when fixing all this, and it will make our comparisons fair.

Maxime Dénès (Mar 31 2017 at 15:42):

What do you think of my plan above?

Pierre-Marie Pédrot (Mar 31 2017 at 15:42):

Right, but we need to document that it is written that way to conform to what the kernel does.

Maxime Dénès (Mar 31 2017 at 15:42):

Yes

Pierre-Marie Pédrot (Mar 31 2017 at 15:42):

LGTM.

Maxime Dénès (Mar 31 2017 at 15:42):

You can even add a technical note that it is probably broken for REVERTcasts...

Maxime Dénès (Mar 31 2017 at 15:47):

Do you need help somewhere in the plan?

Pierre-Marie Pédrot (Mar 31 2017 at 15:48):

I'll have a hard time compiling HoTT but I think I can survive. What is the status of HoTT wrt trunk?

Maxime Dénès (Mar 31 2017 at 15:53):

you can easily use the ci target for that

Maxime Dénès (Mar 31 2017 at 15:54):

make ci-hott

Maxime Dénès (Mar 31 2017 at 15:54):

and thank @Emilio Jesús Gallego Arias ;)

Pierre-Marie Pédrot (Mar 31 2017 at 15:54):

Cool!

Pierre-Marie Pédrot (Mar 31 2017 at 15:55):

Still, I'm finishing Nsatz up. I'm almost done.

Maxime Dénès (Mar 31 2017 at 15:56):

grrrrrrrrrr

Pierre-Marie Pédrot (Mar 31 2017 at 15:56):

If you guys stop distracting me sending messages. The notification thingy is really disturbing.

Emilio Jesús Gallego Arias (Mar 31 2017 at 16:30):

@Pierre-Marie Pédrot disable it; I've done so indeed

Emilio Jesús Gallego Arias (Mar 31 2017 at 17:03):

So indeed @Pierre-Marie Pédrot when you have a bit of free time, I would appreciate knowing more about why ltac needs to store glob_expr, in fact, as you folks know we have this little gem in intf:

(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
   in the environment by the effective calls to Intro, Inversion, etc
   The [constr_expr] field is [None] in TacDef though *)
type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option

thus something is going on, this seems to suggest indeed that ltac may do not so bad without glob_constr.

Pierre-Marie Pédrot (Mar 31 2017 at 22:58):

I'm implementing the delayed universe stuff and I think universe handling in tactics is almost as broken as evars are.

Pierre-Marie Pédrot (Mar 31 2017 at 22:58):

Luckily, almost nobody relies on this as of today, except people doing universe polymorphism.

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:25):

O_O

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:27):

Well you are indeed lucky, I have discovered that exception printing CErrors.iprint performs _essential_ side-effects, so if don't "print" exceptions (relying instead on feedback) then something strange happens between Proof_global and the STM resilience stuff and IDE messages are not emitted anymore.

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:27):

How much fun!

Pierre-Marie Pédrot (Mar 31 2017 at 23:28):

It's Friday, Friday, Friday, gonna get fun fun fun...

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:31):

Never had a Friday like this

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:32):

of course, purely imperative programming couldn't be far from my fun

Pierre-Marie Pédrot (Mar 31 2017 at 23:32):

Chasing bugs on Friday night is a well-known practice!

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:32):

in this particular case, we are talking about _purely imperative error handling_

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:33):

@Pierre-Marie Pédrot my few remaining friends don't approve of it thou

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:33):

ok got it: purely imperative programming, case 2 vs expected case 0

Pierre-Marie Pédrot (Mar 31 2017 at 23:33):

Come on, the EXTASIS of finding that $%!§£ universe leak...

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:34):

"extasis" falls short of describing what you can feel

Pierre-Marie Pédrot (Mar 31 2017 at 23:34):

Not close to it yet unluckily.

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:35):

but yeah I have a better idea we should implement the proof-engine CPS by raising exceptions and attaching properties to them; we could even efficiently implement LTAC with that approach

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:35):

and would likely be cleaner

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:38):

well, I sadly need to go back to my .tex files

Pierre-Marie Pédrot (Mar 31 2017 at 23:38):

Good luck...

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:39):

but I'll share my findings here: the behavior of the STM was essentially different depending whether the toplevel was printing exceptions or not. That was a bit puzzling and was hindering my efforts on the way to a unified printing path. So what happens is that actually printing an exception in Coq, raises other exceptions.

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:39):

Thanks PM!

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:40):

well, that is a bad side effect, but no so bad as to alter the behavior of the STM in such a bad way. Now let me introduce:

purely imperative programming: AKA, Stm.State.define and
purely imperative error handling: AKA, Exninfo.add

Pierre-Marie Pédrot (Mar 31 2017 at 23:40):

Yeah, I wrote Exninfo.add.

Pierre-Marie Pédrot (Mar 31 2017 at 23:41):

That's a horrible hack, but there is no easy way around in OCaml API AFAIK.

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:41):

Now it is essential you put all these ingredients together, and the chain of events is like this:

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:43):

in its purely imperative programming crusade, Stm.State.define will actually run its generic function (of type unit -> unit) and check for any produced exception. Then, it will look at what the properties the resulting exception are, and act in four different, carefully random ways.

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:44):

then error printing comes in the way. A typical pattern in Coq error printers is to raise a new exception inside the handler to delegate the printing to a lower level. That is fine, however, our purely imperative engine is watching, and our finely decorated original exception will be turn into an exception stripped of any attributes if we dare to call the printer.

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:45):

and like due to its randomness, define only does the right thing when indeed the incoming exception is stripped of any attribute.

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:45):

Here you have it.

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:45):

Lots and lots of imperative fun

Pierre-Marie Pédrot (Mar 31 2017 at 23:45):

Yes, we need to take advantage of the new exception uid to use maps instead of reraising exceptions.

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:46):

You got me =>

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:47):

Exninfo.add was written to support reraise, that is fine I think (even if in Ocaml 4.03 we can use the native reraise I think)

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:47):

however Exninfo.add has been badly abused in the STM

Pierre-Marie Pédrot (Mar 31 2017 at 23:47):

Well, the original implementation, believe me or not, was pure;

Pierre-Marie Pédrot (Mar 31 2017 at 23:47):

Unluckily, it relied on OCaml < 4.01 representation of exceptions

Pierre-Marie Pédrot (Mar 31 2017 at 23:48):

and used unsafe machinery to mangle exceptions.

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:49):

Yeah I had a look some weeks ago, I think the original implementation and purpose was fine, however you should have restricted Exninfo.add so people cannot abuse it

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:49):

people^W the STM

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:49):

in fact yeah it seems badly broken

Pierre-Marie Pédrot (Mar 31 2017 at 23:50):

now that we have PPX we may try do that by using a wrapper

Pierre-Marie Pédrot (Mar 31 2017 at 23:50):

ensuring that all try / with are guarded

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:50):

what about doing external reraise : exn -> 'a = "%reraise"

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:50):

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:51):

oh well you mean for catchable ones, that would be fine

Pierre-Marie Pédrot (Mar 31 2017 at 23:51):

this needs to ensure that no exception was raised in the meantime

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:52):

thou it seems that if people forget to use the guard they could forget to use the ppx

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:53):

Anyways, IMO attaching backtraces is fine, attaching locations is quite fragile but could be allowed (worse effect you lose location info), attaching properties the way the STM does is just broken now, unless we change a lot of things in Coq to ensure properties are preserved in exception "transformers"

Pierre-Marie Pédrot (Mar 31 2017 at 23:54):

I never got the whole stuff about exception wrapping in the STM

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:56):

Yeah I think we want to remove it, it is just impossible to make it reliable due the semantics of state + reliance on preservation of the attachemente

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:57):

so you say PM that %reraise wouldn't work would we move to 4.03?

Pierre-Marie Pédrot (Mar 31 2017 at 23:57):

The problem is that you may want to reraise an exception after having done something.

Pierre-Marie Pédrot (Mar 31 2017 at 23:57):

If ever that something raises an exception, you can say farewell to the attached backtrace.

Emilio Jesús Gallego Arias (Mar 31 2017 at 23:58):

I see

Emilio Jesús Gallego Arias (Apr 01 2017 at 00:00):

thx

Emilio Jesús Gallego Arias (Apr 01 2017 at 00:02):

So would you support a change towards type iexn = exn * Backtrace.t ?

Pierre-Marie Pédrot (Apr 01 2017 at 00:03):

You may want other irrelevant information than Backtrace, e.g. locations.

Pierre-Marie Pédrot (Apr 01 2017 at 00:04):

What one should not do is to rely on the info parameter to take decisions

Pierre-Marie Pédrot (Apr 01 2017 at 00:04):

That is only for debug or printing.

Emilio Jesús Gallego Arias (Apr 01 2017 at 00:09):

Ok, we fully agree on that. Regarding locations, I'd weakly push for removing that in favor of a located object:

It is not used a lot.
Exceptions are really the wrong way to handle locations, as location information is also necessary on many non-error paths.

Emilio Jesús Gallego Arias (Apr 01 2017 at 00:09):

but yeah that is very low priority

Emilio Jesús Gallego Arias (Apr 01 2017 at 00:09):

the stm stuff is of higher priority thou

Pierre-Marie Pédrot (Apr 01 2017 at 00:10):

Do as you prefer, I can't say I'm fond of this code.

Pierre-Marie Pédrot (Apr 01 2017 at 00:22):

Aha! Got my bug.

Pierre-Marie Pédrot (Apr 01 2017 at 00:22):

Morale: how is it possible to write correct code without the help of a proof assistant?

Emilio Jesús Gallego Arias (Apr 01 2017 at 00:30):

:D seems a bit like a chicken and egg problem :D

Pierre-Marie Pédrot (Apr 01 2017 at 00:31):

It's a miracle that Coq is not yet bootstrapped.

Pierre-Marie Pédrot (Apr 01 2017 at 00:31):

50 years from now, people will look at us with a mix of compassion and contempt

Pierre-Marie Pédrot (Apr 01 2017 at 00:32):

In ye olde days, we were cowboys !

Pierre-Marie Pédrot (Apr 01 2017 at 00:32):

« À l’époque, j’étais moi-même cowboy, je vivais avec Jacques, un bon copain. »

Maxime Dénès (Apr 01 2017 at 00:47):

@Pierre-Marie Pédrot Did you confirm the inefficiency in HoTT and others come from universe normalization

Pierre-Marie Pédrot (Apr 01 2017 at 00:47):

Working on it.

Pierre-Marie Pédrot (Apr 01 2017 at 00:47):

I've already stopped normalizing universes, and on my way to instances.

Maxime Dénès (Apr 01 2017 at 00:47):

but you do that by implementing the lazy universe normalization?

Pierre-Marie Pédrot (Apr 01 2017 at 00:47):

Yes.

Pierre-Marie Pédrot (Apr 01 2017 at 00:47):

This is always going to be more efficient.

Maxime Dénès (Apr 01 2017 at 00:47):

I would have used a profiling tool.

Pierre-Marie Pédrot (Apr 01 2017 at 00:48):

Even for non-universe polymorphic code.

Maxime Dénès (Apr 01 2017 at 00:48):

Yes, but here again you are going to find cases where code relies on the wrong behavior, right?

Pierre-Marie Pédrot (Apr 01 2017 at 00:48):

For now, this looks OK.

Pierre-Marie Pédrot (Apr 01 2017 at 00:48):

I'm pretty sure we'll wreak havoc in HoTT, but I'm a believer.

Maxime Dénès (Apr 01 2017 at 00:48):

Ok. I agree that's something we need to fix anyway, but I'm a bit afraid to open a second front in the middle of the EConstr war.

Pierre-Marie Pédrot (Apr 01 2017 at 00:49):

Finger in the gear, they say...

Maxime Dénès (Apr 01 2017 at 00:50):

Well, if that is the only way, then fine, but if using a profiler shows another source of inefficiency... We'd better fix that one and merge EConstr first.

Pierre-Marie Pédrot (Apr 01 2017 at 00:50):

I'm really sure this is because of that.

Pierre-Marie Pédrot (Apr 01 2017 at 00:50):

I mean this affects specifically HoTT, and it is clear from the code what happens.

Maxime Dénès (Apr 01 2017 at 00:50):

Gotta sleep, but keep me posted please, I'll try to help you, even with a second front :)

Maxime Dénès (Apr 01 2017 at 00:52):

I'm only a second couteau in this stuff, but I have no mercy.

Pierre-Marie Pédrot (Apr 01 2017 at 00:52):

And need no sleep, I see

Emilio Jesús Gallego Arias (Apr 01 2017 at 01:10):

Maxime stop interrupting PM, he's trying to work !

Jason Gross (Apr 01 2017 at 04:36):

@Emilio Jesús Gallego Arias (@05:04) HoTT has a way of spitting out .timing files (maybe make timing; I don't recall; it just saves the output of coqc -time), but there's nothing that processes them to create diffs. It shouldn't be too hard to extend my timing python scripts to handle .timing files; you just need to teach it about the output format of coqc -time, in addition to the output of make TIMED=1.

Jason Gross (Apr 01 2017 at 04:39):

@Pierre-Marie Pédrot (11:38) What's wrong with the invariant in casts? To me it says that consecutive VM/native casts should be coalesced (which can only ever make typechecking faster, because these casts fully normalize the types and so it doesn't matter what type you claim to be casting to/from), but other casts should not be coalesced (because if they are, you might blow up conversion, because you've lost the careful hints the user inserted to guide conversion to not taking forever)

Jason Gross (Apr 01 2017 at 04:42):

Unrelatedly, I managed to trigger the assert in pretyping/constr_matching.ml in this function:

let rec extract_bound_aux k accu frels ctx = match ctx with
| [] -> accu
| (na1, na2, _) :: ctx ->
  if Int.Set.mem k frels then
    begin match na1 with
    | Name id ->
      let () = assert (match na2 with Anonymous -> false | Name _ -> true) in
      let () = if Id.Set.mem id accu then raise PatternMatchingFailure in
      extract_bound_aux (k + 1) (Id.Set.add id accu) frels ctx
    | Anonymous -> raise PatternMatchingFailure
    end
  else extract_bound_aux (k + 1) accu frels ctx

The trigger condition seems to have something to do with match statements. I'm working on minimizing the bug, but was wondering if any of you all have any thoughts on what this means.

Emilio Jesús Gallego Arias (Apr 01 2017 at 05:04):

We should get @herbelin here

Emilio Jesús Gallego Arias (Apr 01 2017 at 05:04):

I think he's the one that may know, maybe Matthieu too?

Emilio Jesús Gallego Arias (Apr 01 2017 at 05:05):

I guess @Théo Zimmermann can lure him in

Théo Zimmermann (Apr 01 2017 at 10:35):

Sorry I won't be back to the office until Wednesday, so I can't be of any physical help here.

Théo Zimmermann (Apr 01 2017 at 10:36):

@Matthieu Sozeau is supposed to be on this chat though, but he's never said anything so I'm not sure he'll see the notification

Théo Zimmermann (Apr 01 2017 at 16:27):

Do you guys know about git fetch origin pull/PRNUMBER/head? I just learned about it in the nixpkgs manual.

Pierre-Marie Pédrot (Apr 01 2017 at 16:27):

Actually I use some magic config line that allows me to see PR as github/pr/#NUM.

Théo Zimmermann (Apr 01 2017 at 16:28):

So far, to test a PR I always added a new remote corresponding to the submitter's fork :S

Pierre-Marie Pédrot (Apr 01 2017 at 16:28):

Magic line:

[remote "github"]
        url = git@github.com:coq/coq.git
        fetch = +refs/heads/*:refs/remotes/github/*
        fetch = +refs/pull/*/head:refs/remotes/github/pr/*

Théo Zimmermann (Apr 01 2017 at 16:28):

@Pierre-Marie Pédrot I'd be interested in your config line.

Théo Zimmermann (Apr 01 2017 at 16:29):

cool thanks!

Pierre-Marie Pédrot (Apr 01 2017 at 16:29):

The important line is the third one.

Théo Zimmermann (Apr 01 2017 at 16:34):

yeah I figured out (after some comparison to existing configuration)

Théo Zimmermann (Apr 01 2017 at 16:48):

I wonder if there is a way to see only opened PRs

Jason Gross (Apr 01 2017 at 17:30):

@Théo Zimmermann I doubt it. The comments on https://gist.github.com/piscisaureus/3342247 suggest other people are looking for a way and haven't found one, and I don't think github has separate URLs for open vs closed pull requests (everything is https://github.com/coq/coq/pull/n) so I don't think you can use any sort of wild-card filter to separate open ones from closed ones. It might be possible to wrangle some sort of hook that goes and separately looks at the github data and deletes the local refs for PRs that aren't open, but git doesn't seem to have a post-fetch hook, so that seems like a non-starter. Maybe you could write a bash script that fetches the PRs and then deletes the ones that are closed? ¯\_(ツ)_/¯

Théo Zimmermann (Apr 01 2017 at 17:31):

Thanks @Jason Gross! That's quite useful information.

Théo Zimmermann (Apr 01 2017 at 18:14):

after weighing in several solutions, I'm going to go with a git alias:

pull-request = "!f() { git fetch -fu ${2:-$(git remote | grep ^upstream || echo origin)} refs/pull/$1/head && git checkout --detach FETCH_HEAD; }; f"

Théo Zimmermann (Apr 01 2017 at 18:15):

this will avoid me fetching too many PRs

Pierre-Marie Pédrot (Apr 01 2017 at 18:26):

@Maxime Dénès I've pushed the delayed universe fix on my branch. I'll try to schedule a benchmark on pendulum.

Pierre-Marie Pédrot (Apr 01 2017 at 18:26):

AFAICT HoTT still compiles, which is a good thing...

Maxime Dénès (Apr 01 2017 at 20:07):

@Pierre-Marie Pédrot Nice! Let me know how it goes.

Pierre-Marie Pédrot (Apr 01 2017 at 20:08):

pendulum is a bit crowded at the time...

Pierre-Marie Pédrot (Apr 01 2017 at 20:09):

Is fiat-crypto supposed to compile with trunk? I keep getting a stack overflow on my machine.

Pierre-Marie Pédrot (Apr 01 2017 at 20:09):

in ./src/WeierstrassCurve/WeierstrassCurveTheorems.v

Pierre-Marie Pédrot (Apr 01 2017 at 20:10):

And strangely enough, Travis fails on my clean-nsatz branch while it works for me...

Pierre-Marie Pédrot (Apr 01 2017 at 20:11):

File "./src/Util/WordUtil.v", line 67, characters 4-17:
Error: Ltac call to "etransitivity" failed.
       No matching clauses for match.

Jason Gross (Apr 01 2017 at 21:47):

@Pierre-Marie Pédrot Let me compile the latest trunk and try it on the latest fiat-crypto. (Should definitely build on v8.6, as long as you have enough time and enough ram.)

Pierre-Marie Pédrot (Apr 01 2017 at 21:48):

I have a patch to make it work in any case. The stack overflow comes from a call to List.merge in ideal.ml.

Jason Gross (Apr 01 2017 at 21:50):

@Pierre-Marie Pédrot Nice!

Jason Gross (Apr 01 2017 at 21:50):

Also, I managed to track down the anomaly in constr_matching; seems like there's an invariant that's asserted there that the vm breaks: https://coq.inria.fr/bugs/show_bug.cgi?id=5434

Matej Košík (Gitter import) (Apr 02 2017 at 13:38):

@Pierre-Marie Pédrot @Maxime Dénès Pendulum is yearning for more benchmarking jobs ... You can queue in advance any number of jobs.

Pierre-Marie Pédrot (Apr 02 2017 at 16:09):

@Matej Košík Is HoTT supposed to compile with master? I launched a bench yesterday for EConstr but HoTT was not compiled. Looking at the list of default benched packages, it does not appear there...

Matej Košík (Gitter import) (Apr 02 2017 at 17:49):

@Pierre-Marie Pédrot Let me check ...
(I think I dropped it from the set of default OPAM package at some point by mistake).

Pierre-Marie Pédrot (Apr 02 2017 at 18:03):

I think I already harassed some of you at POPL about this, to no avail, and I'm becoming crazy. To be short, the 'perf' tool does not work anymore for me after going from a 4.8 kernel to a 4.9 kernel. This is an important tool for profiling Coq, and I'd like not to be stuck on an already old kernel. Do anyone of you know where I could find some help?

Pierre-Marie Pédrot (Apr 02 2017 at 18:04):

There is no Debian bug on perf, and I can't find anything related to my problems through the allmighty Google.

Jason Gross (Apr 02 2017 at 18:11):

@Pierre-Marie Pédrot @Matej Košík There's a branch of @Emilio Jesús Gallego Arias 's that has HoTT compiling with 8.6, and another one that has it compiling with master? I think we plan to integrate the 8.6 branch as soon as we can integrate a version of dpdgraph that works with 8.6.

Matej Košík (Gitter import) (Apr 02 2017 at 18:15):

@Jason Gross yes and yes.

Matej Košík (Gitter import) (Apr 02 2017 at 18:17):

I am not sure if I understand your plans. From my (not very well informed) point of view, it would be great if we did not have to use our custom branches but we could directly clone your repo and test it with Coq 8.6 & trunk.

Matej Košík (Gitter import) (Apr 02 2017 at 18:22):

@Pierre-Marie Pédrot I've checked, Emilio's branch of coq-hott still compiles with Coq trunk. I've added it (back) among the default OPAM-packages for benchmarking.

Pierre-Marie Pédrot (Apr 02 2017 at 18:23):

OK, thanks, I'll retry a bench for EConstr.

Jason Gross (Apr 02 2017 at 21:36):

The thing currently blocking me from integrating the patch that makes HoTT compile with 8.6 is the fact that the make install-coqlight target went away. @Emilio Jesús Gallego Arias suggested using

make states tools
touch bin/coqtop.byte bin/coqchk stm/{proof,tac,query}workertop.cma
sudo make install-binaries
sudo rsync -a plugins theories /usr/local/lib/coq/

but this fails to build/install grammar/compat5.cmo, which is needed for coq-dpdgraph. How should I build and install coq without building all of the standard library in a way that gets me compat5.cmo?

Emilio Jesús Gallego Arias (Apr 02 2017 at 23:16):

@Jason Gross does the install-library target work? I'll try to clean up the makefile situation one of these days so we don't need such hacks.

Jason Gross (Apr 02 2017 at 23:18):

My current solution is make states tools coqlight plugins grammar/compat5.cmo grammar/grammar.cma and make install-binaries install-devfiles, which seems to work. I'm now trying to fix the issue that trusty ocaml doesn't support -safe-string (which coq-dpdgraph unconditionally passes)

Emilio Jesús Gallego Arias (Apr 02 2017 at 23:27):

it is the coq makefile which actually passes the -safe-string flag, and indeed building coq plugings with a different -safe-string setting is not supported. Note that Coq 8.7 requires ocaml 4.02.3, which supports safe string. My advice is to use the standard ocaml repos for travis as used in Coq's travis.yml

Jason Gross (Apr 02 2017 at 23:31):

@Emilio Jesús Gallego Arias What do you mean it is coq_makefile? https://github.com/Karmaki/coq-dpdgraph/blob/master/Makefile.in#L50

Jason Gross (Apr 02 2017 at 23:33):

Alternatively, @Emilio Jesús Gallego Arias , do you want to take over finishing up the port to 8.6? I've pushed a bunch of commits on top of your branch at https://github.com/JasonGross/HoTT/tree/mz-8.6 (feel free to squash all of mine into one, or not, at your discretion), and the only thing left, I think, is actually getting coq-dpdgraph to build on travis.

Emilio Jesús Gallego Arias (Apr 02 2017 at 23:37):

Indeed I meant that in trunk coq_makefile will force plugins to be built with -safe-string. You can build a plugin with -safe-string even if Coq is not; however the inverse doesn't hold.

Emilio Jesús Gallego Arias (Apr 02 2017 at 23:38):

I've been very busy these days sorry, feel free to take over if you want.

Emilio Jesús Gallego Arias (Apr 02 2017 at 23:38):

Note also the mz-8.7 branch

Emilio Jesús Gallego Arias (Apr 02 2017 at 23:38):

which is the one used for trunk

Emilio Jesús Gallego Arias (Apr 02 2017 at 23:39):

we should eventually get to integrate that one, but not urgent IMO.

Emilio Jesús Gallego Arias (Apr 02 2017 at 23:39):

Indeed I suggest you build the 8.6 branch with the mz-8.7 setup

Emilio Jesús Gallego Arias (Apr 02 2017 at 23:40):

[for travis] that will solve the dpdgraph problem

Jason Gross (Apr 02 2017 at 23:52):

@Emilio Jesús Gallego Arias I don't see anything special about the travis setup in https://github.com/ejgallego/HoTT/tree/mz-8.7 ...

Jason Gross (Apr 02 2017 at 23:54):

Unrelatedly, I think I got burned by relying on behavior of the unifier, and finding it too unpredictable. When documenting my code as part of a PR for fiat-crypto, I added this paragraph to explain this line of code:

       (** Now we rely on the behavior of Coq's unifier to transform
           the goal for us; we a goal like [let f' : A := ?f_evar in
           B], and we want a goal like [A /\ B].  So we refine with a
           hole named [pf] which is proof of [A /\ B], and then assert
           that the second projection of the proof (which has type
           [B]) actually has type [let f' : A := proj1 pf in B].  If
           done naïvely, this would give a circlular type, which Coq
           disallows.  However, Coq is happy to zeta-reduce away the
           circlularity; happily, this is done after Coq unifies [let
           f' : A := proj1 pf in B] with [let f' : A := ?f_evar in B],
           hence filling [?f_evar] with the first projection of the
           proof.  Since Coq instantiates the two existing evars
           ([?f_evar] and the current goal, which is represented by an
           evar under the hood) with projections of the new evar
           (which becomes the new goal)---and let us hope that Coq
           devs never decide both to turn on judgmental η (currently
           controlled by primitive projections) for [and], and to
           prefer η-expansion of evars before dropping context
           variables (we might also be in trouble if someone adds a
           [Canonical Structure] for [and])---we get the desired
           behavior--for now. *)
       lazymatch goal with
       | [ |- let f' := _ in ?B ]
         => refine (let pf := _ in (proj2 pf : let f' := proj1 pf in B))
       end

Now I'm trying to fix an issue where Defined takes over 30 hours and over 10 GB of RAM, and it seems like this one refine is the issue...

Emilio Jesús Gallego Arias (Apr 03 2017 at 00:27):

@Jason Gross oh sorry I meant this branch: https://github.com/ejgallego/HoTT/tree/ocaml.4.02.3

Emilio Jesús Gallego Arias (Apr 03 2017 at 00:31):

@Jason Gross , related unification indeed there has been recent general chat about whether Coq users can really rely on unification. The impression is that with the current status of the heuristics it is not a good idea. I am not really qualified to talk about this given that many expert people is in the chat, but coming from a Logic Programming background, indeed we rely on predictable unification, but AFAICT the closest you can do in Coq is UniCoq, and even it, it may be not too stable yet. But one of the pitfalls of logic programming is the way unification and backtracking break modularity. In fact this is why I stopped writing Prolog and LProlog programs. If you try to update unification, it is common to have to update all your programs, and this is not what you want when writing proofs. I won't get started with backtracking....

Jason Gross (Apr 03 2017 at 00:31):

@Emilio Jesús Gallego Arias Thanks for the pointer re HoTT

Jason Gross (Apr 03 2017 at 00:33):

@Emilio Jesús Gallego Arias re unification the behavior I'm relying on here is that if you try to unify let f := x in y with let f := ?e in y, where ?e is an evar (and the only one), then Coq will instantiate ?e with x rather than preemptively doing zeta-reduction and discovering that f does not occur in y and so it doesn't need to instantiate ?e.

Emilio Jesús Gallego Arias (Apr 03 2017 at 00:33):

@Jason Gross NP!! I indeed see no reason as not to push the updates in https://github.com/ejgallego/HoTT/commit/b2255e1feca65b7eb01dab5484a712eac4dea33f

Jason Gross (Apr 03 2017 at 00:35):

Why this makes Defined take forever, I don't know

Jason Gross (Apr 03 2017 at 00:35):

(see https://coq.inria.fr/bugs/show_bug.cgi?id=5437 for more details)

Emilio Jesús Gallego Arias (Apr 03 2017 at 00:35):

@Jason Gross re unif: that looks pretty fragile to me in the presence of the other heuristics, [that could be triggered non-locally] but I'm sure experts will comment on that.

Jason Gross (Apr 03 2017 at 00:37):

What's non-local? I rely on this only at top-level, in the case where I do refine (let pf := _ in ((_ : T2) : T3)) where T2 is of the form let f := x in y and T2 is of the form let f := ?e in y

Jason Gross (Apr 03 2017 at 00:37):

*and T3 is of the form

Jason Gross (Apr 03 2017 at 00:47):

@Emilio Jesús Gallego Arias but, yeah, I expected it to be fragile, which is why I wrote such a long comment in the source explaining what I was doing

Pierre-Marie Pédrot (Apr 03 2017 at 10:24):

Is there a way to add VST git repository to the pendulum benchmark? I've no knowledge on writing opam packages...

Maxime Dénès (Apr 03 2017 at 11:22):

@Pierre-Marie Pédrot The problem is that VST does not compile with Coq trunk

Pierre-Marie Pédrot (Apr 03 2017 at 11:54):

Why not? Last time I tried it worked...

Maxime Dénès (Apr 03 2017 at 11:56):

Because we broke Flocq

Maxime Dénès (Apr 03 2017 at 11:57):

We fixed Flocq, ported the fix to CompCert which embeds Flocq, but did not port the fix to VST which embeds CompCert...

Pierre-Marie Pédrot (Apr 03 2017 at 11:57):

I've submitted a PR to backport already : https://github.com/PrincetonUniversity/VST/pull/68

Pierre-Marie Pédrot (Apr 03 2017 at 11:57):

and it got merged.

Maxime Dénès (Apr 03 2017 at 11:57):

oh!

Maxime Dénès (Apr 03 2017 at 11:58):

So I don't know, @Matej Košík, why doesn't the bench compile VST?

Pierre-Marie Pédrot (Apr 03 2017 at 11:58):

AFAIK, there is no opam package.

Maxime Dénès (Apr 03 2017 at 11:58):

@Pierre-Marie Pédrot what is the status of EConstr?

Pierre-Marie Pédrot (Apr 03 2017 at 11:58):

Waiting for a bench on HoTT

Pierre-Marie Pédrot (Apr 03 2017 at 11:59):

I'm expecting time gain for everybody (hopefully).

Maxime Dénès (Apr 03 2017 at 11:59):

What build is it on Jenkins?

Pierre-Marie Pédrot (Apr 03 2017 at 12:00):

#102

Pierre-Marie Pédrot (Apr 03 2017 at 12:01):

101 is evaluating the removal of double hashconsing essentially, but I'd like to test it on VST as well, so it can probably be cancelled if you're in a hurry about EConstr.

Maxime Dénès (Apr 03 2017 at 12:03):

Ok I'll interrupt it.

Maxime Dénès (Apr 03 2017 at 12:05):

We should put only one iteration for benchmarks

Pierre-Marie Pédrot (Apr 03 2017 at 12:05):

All right, I thought 3 was coming from some rule of thumb.

Maxime Dénès (Apr 03 2017 at 12:06):

Also, beware that when you use "benchmark-the-whole-branch", bash script tries to guess the base branch it should compare against

Pierre-Marie Pédrot (Apr 03 2017 at 12:06):

Should we ensure master is merged before benching then?

Maxime Dénès (Apr 03 2017 at 12:16):

No, precisely if you do that you'll run into trouble.

Maxime Dénès (Apr 03 2017 at 12:16):

I advice you double check the base commit in all the benchmark results you got so far.

Maxime Dénès (Apr 03 2017 at 12:16):

You may be comparing two unrelated branches...

Pierre-Marie Pédrot (Apr 03 2017 at 12:22):

Fine, I'm leaving the dirty work to you for now then.

Pierre-Marie Pédrot (Apr 03 2017 at 12:26):

@Maxime Dénès Should I perfom a merge into EConstr anyway?

Maxime Dénès (Apr 03 2017 at 12:40):

I did it recently, so it won't change much

Maxime Dénès (Apr 03 2017 at 12:41):

@Pierre-Marie Pédrot Btw , why didn't we try to merge a version of EConstr that was doing the same normalization of universes as Constrs before? (not more) Was there any difficulty?

Pierre-Marie Pédrot (Apr 03 2017 at 12:42):

That's probably unsound now that we removed eager normalization.

Pierre-Marie Pédrot (Apr 03 2017 at 12:42):

That said, I would not be surprised if the code in master is deadly bugged.

Pierre-Marie Pédrot (Apr 03 2017 at 12:42):

It probably still is in EConstr, though a bit less.

Enrico Tassi (Apr 03 2017 at 12:43):

If we don't remove nf_evar from here and there, but leave EConstr.kind there and doing only evar-related work (no univ work)

Enrico Tassi (Apr 03 2017 at 12:43):

wouldn't that be sound?

Pierre-Marie Pédrot (Apr 03 2017 at 12:43):

Probably not anyway.

Enrico Tassi (Apr 03 2017 at 12:43):

would it be less sound than without econstr?

Maxime Dénès (Apr 03 2017 at 12:44):

Well, I don't think we can measure things like that.

Pierre-Marie Pédrot (Apr 03 2017 at 12:44):

I'd say on the same order of magnitude.

Pierre-Marie Pédrot (Apr 03 2017 at 12:44):

Fact is, nobody is using universe polymorphism.

Enrico Tassi (Apr 03 2017 at 12:44):

I mean: more bugs, same bugs, different bugs

Pierre-Marie Pédrot (Apr 03 2017 at 12:44):

Except crazy people who don't care yet about another buggy unification

Maxime Dénès (Apr 03 2017 at 12:44):

It will be unsound in a different way, which means breaking code to replace unsoundness by unsoundness...

Pierre-Marie Pédrot (Apr 03 2017 at 12:45):

Maxime Dénès (Apr 03 2017 at 12:45):

(in the few developments that actually use univ poly)

Enrico Tassi (Apr 03 2017 at 12:45):

I still don't get where the change would come

Enrico Tassi (Apr 03 2017 at 12:45):

from

Pierre-Marie Pédrot (Apr 03 2017 at 12:46):

Typically, if you unify some universe variable with Set / Prop, then you're going to be able to observe that.

Pierre-Marie Pédrot (Apr 03 2017 at 12:46):

I think I spotted an instance of this bug somewhere, or at least imagined I had seen it in the wild.

Enrico Tassi (Apr 03 2017 at 12:47):

sorry, I did not make the context of my question clear

Enrico Tassi (Apr 03 2017 at 12:47):

objective: merge the API change of econstr, without attempting to fix any bug in existing code, nor introducing new bugs

Pierre-Marie Pédrot (Apr 03 2017 at 12:48):

@Enrico Tassi I don't believe this is feasible.

Maxime Dénès (Apr 03 2017 at 12:48):

well the question is: with how much code duplication?

Maxime Dénès (Apr 03 2017 at 12:48):

in particular, if you don't want to duplicate all the primitives (reduction, occur functions, etc.)

Pierre-Marie Pédrot (Apr 03 2017 at 12:48):

Yeah obviously you can duplicate all folders starting from engine

Pierre-Marie Pédrot (Apr 03 2017 at 12:49):

We don't want to do that, do we?

Maxime Dénès (Apr 03 2017 at 12:49):

as soon as you look for occurrences of variables in properly substituted terms, you change unification...

Maxime Dénès (Apr 03 2017 at 12:49):

it is so broken!

Pierre-Marie Pédrot (Apr 03 2017 at 12:50):

Welcome in Coq Hell, Mr Anderson.

Pierre-Marie Pédrot (Apr 03 2017 at 12:50):

« Les *bugs peuvent prendre de nombreuses formes ! Ce n'est que le début, M. Vincent. »

Maxime Dénès (Apr 03 2017 at 12:51):

@Pierre-Marie Pédrot please repeat what you said here in #526 about the proper datatype to use

Maxime Dénès (Apr 03 2017 at 12:51):

it is an interesting and underdocumented issue

Pierre-Marie Pédrot (Apr 03 2017 at 12:52):

I already forgot. How can we find something in the history of the chat?

Maxime Dénès (Apr 03 2017 at 12:52):

"Search Gitter" in the leftside panel

Enrico Tassi (Apr 03 2017 at 12:54):

@Pierre-Marie Pédrot why is that impossible? I mean you don't port evarconv for for example (you change the API taking an econstr, then you immediately Unsafe.to_constr)

Maxime Dénès (Apr 03 2017 at 12:54):

@Enrico Tassi I started to do that for real

Enrico Tassi (Apr 03 2017 at 12:54):

... and...

Maxime Dénès (Apr 03 2017 at 12:54):

I can show you the code, I gave up after two days of work

Maxime Dénès (Apr 03 2017 at 12:55):

and like 10+ hours each day sitting at the desk

Maxime Dénès (Apr 03 2017 at 12:55):

I got something that compiled and failed on the stdlib...

Enrico Tassi (Apr 03 2017 at 12:57):

so which is the future of econstr?

Maxime Dénès (Apr 03 2017 at 12:57):

it is this: https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/21/console

Pierre-Marie Pédrot (Apr 03 2017 at 12:57):

@Enrico Tassi I'd favour merging and seeing if we broke things.

Maxime Dénès (Apr 03 2017 at 12:57):

more precisely, we fixed the last known incompatibilities

Maxime Dénès (Apr 03 2017 at 12:58):

now we'd like to fix the performance overhead

Enrico Tassi (Apr 03 2017 at 12:58):

this branch includes the removal of some nf_evar, fixes to pretyping, ...

Enrico Tassi (Apr 03 2017 at 12:58):

all that?

Maxime Dénès (Apr 03 2017 at 12:58):

yes

Pierre-Marie Pédrot (Apr 03 2017 at 12:58):

It's very intricate, I agree.

Enrico Tassi (Apr 03 2017 at 12:59):

well good luck

Pierre-Marie Pédrot (Apr 03 2017 at 12:59):

But that's what you get when you have to fix years of shitty code.

Enrico Tassi (Apr 03 2017 at 12:59):

I only partially agree, IMO you did look for troubles ;-)

Pierre-Marie Pédrot (Apr 03 2017 at 13:00):

I think we really had to do this at some point.

Pierre-Marie Pédrot (Apr 03 2017 at 13:00):

@Maxime Dénès can probably write a whole book about the eldritch horrors of unification.ml.

Pierre-Marie Pédrot (Apr 03 2017 at 13:02):

I'm not sure I'm willing to answer the discussion on funind actually...

Pierre-Marie Pédrot (Apr 03 2017 at 13:04):

Let them merge their code, and at some point kick funind out the repo.

Maxime Dénès (Apr 03 2017 at 13:23):

@Enrico Tassi do you think it is the right strategy for funind, what PMP suggests?

Pierre-Marie Pédrot (Apr 03 2017 at 13:25):

If I can put a bit more argumentation on the table:

You don't make drink a donkey who's not thirsty.
This code is not fixable, however much energy we'll put in it.
Most people use it for very basic needs (and actually virtually anything else raises anomalies)

Théo Zimmermann (Apr 03 2017 at 13:29):

there is a project to merge Function, Equations, and Program Fixpoint on the roadmap.

Enrico Tassi (Apr 03 2017 at 13:33):

I've no opinion/knowledge on funind. To my eyes it is made of copy/paste, i.e. very bad code, but I did never dig deep. IMO what @Pierre-Marie Pédrot proposes is reasonable.

Maxime Dénès (Apr 03 2017 at 14:31):

I'm ok, but it means no communicating. We let people work on it, while hoping that we get rid of the code...

Maxime Dénès (Apr 03 2017 at 14:32):

Also, I'm not sure if this unification project @Théo Zimmermann mentions is really going to happen. The actors were @Matthieu Sozeau and Yves, and AFAIK they have very little time available.

Théo Zimmermann (Apr 03 2017 at 14:33):

Yes, I suppose the same fate awaits the unification of the unification algorithms.

Théo Zimmermann (Apr 03 2017 at 14:34):

Although, this could happen in a later release.

Maxime Dénès (Apr 03 2017 at 14:34):

Yeah, for funind the situation is looking a bit better: @Matthieu Sozeau has hired an engineer to work on it. But it still requires time from some senior devs.

Maxime Dénès (Apr 03 2017 at 14:35):

@Matej Košík WTF? Isn't HoTT in the default packages for the bench?

Théo Zimmermann (Apr 03 2017 at 14:36):

Already! Great news. Where did he found the money for it?

Maxime Dénès (Apr 03 2017 at 14:36):

I'm wasting my time waiting for the bench since hours.

Maxime Dénès (Apr 03 2017 at 14:36):

I don't know, I wasn't involved in the hiring process

Théo Zimmermann (Apr 03 2017 at 14:37):

OK, well anyways, that's always good to hear that more people are hired for working on Coq, until the Consortium starts.

Maxime Dénès (Apr 03 2017 at 14:42):

Yeah, to say the truth I feel it lacks coordination, on my contract it is written that I should supervise the engineering effort on Coq, and I was aware of this hiring only after it took place.

Maxime Dénès (Apr 03 2017 at 14:50):

But indeed it is always good to get more manpower, we badly need it.

Pierre-Marie Pédrot (Apr 03 2017 at 15:20):

@Maxime Dénès Too late, but if I had been you I'd have waited for the completion and only checked HoTT in a separate run.

Matej Košík (Gitter import) (Apr 03 2017 at 15:29):

@Pierre-Marie Pédrot That's what we did. Intermediate results:

Matej Košík (Gitter import) (Apr 03 2017 at 15:31):

I've sent the intermediate results:

https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/21/console

┌──────────────┬─────────────────────────┬─────────────────────────────────────┬───────────────────────────────────────┐
│              │      user time [s]      │             CPU cycles              │           CPU instructions            │
│              │                         │                                     │                                       │
│ package_name │     NEW     OLD PDIFF   │           NEW           OLD PDIFF   │            NEW            OLD PDIFF   │
├──────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┤
│   coq-geocoq │ 2422.54 2421.81 +0.03 % │ 6741260473927 6743054069790 -0.03 % │ 11272153642487 11437966699056 -1.45 % │
├──────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┤
│ coq-compcert │  838.36  835.39 +0.36 % │ 2328009504172 2317808332890 +0.44 % │  3494804886743  3550565787937 -1.57 % │
└──────────────┴─────────────────────────┴─────────────────────────────────────┴───────────────────────────────────────┘

Fixed the Jenkins's set of default packages (added coq-hott at the beginning)
and restarted Maxime's job with coq-hott and the rest of the packages.

Pierre-Marie Pédrot (Apr 03 2017 at 15:32):

Well, there were quite a few other packages in the run, weren't there?

Matej Košík (Gitter import) (Apr 03 2017 at 15:35):

Benchmarking was finished only for two packages:

coq-geocoq
coq-compcert
The new job, in addition to coq-hott, will benchmark also the remaining ones:

coq-hott coq-color coq-fiat-crypto coq-fiat-parsers coq-flocq coq-unimath coq-sf coq-mathcomp-ssreflect coq-iris coq-mathcomp-fingroup coq-mathcomp-finmap coq-coquelicot coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd_order

Pierre-Marie Pédrot (Apr 03 2017 at 15:36):

All right then. That's slow as hell for two packages...

Matej Košík (Gitter import) (Apr 03 2017 at 15:39):

-j1 :-(

Pierre-Marie Pédrot (Apr 03 2017 at 15:40):

And luckily intuitionistic-nuprl is not in there!

Matej Košík (Gitter import) (Apr 03 2017 at 15:40):

Both of them take a lot of time to finish. Also, each of them is compiled for two Coq commits :-(.

Pierre-Marie Pédrot (Apr 03 2017 at 16:26):

I know I'm nitpicking, but is it possible to cache the timing results for pairs of Coq hashes / package hashes? That way the bench would not have to recompile twice the packages...

Enrico Tassi (Apr 03 2017 at 16:32):

I guess we all need a candy before going home...

Enrico Tassi (Apr 03 2017 at 16:32):

Check forall x : nat, forall x : Prop, x -> x.

Enrico Tassi (Apr 03 2017 at 16:33):

nat -> forall x0 : Prop, x0 -> x0

Matej Košík (Gitter import) (Apr 03 2017 at 16:33):

@Pierre-Marie Pédrot That makes sense.

Enrico Tassi (Apr 03 2017 at 16:33):

;-)

Matej Košík (Gitter import) (Apr 03 2017 at 16:33):

... makes sense

Pierre-Marie Pédrot (Apr 03 2017 at 16:33):

LGTM. Where is the trick?

Pierre-Marie Pédrot (Apr 03 2017 at 16:34):

@Matej Košík Fine for me.

Matej Košík (Gitter import) (Apr 03 2017 at 16:43):

@Enrico Tassi I am afraid my mind was silently alpha-converting. You are right, its lame.

Enrico Tassi (Apr 03 2017 at 17:16):

... the second x is renamed into x0 (to avoid a collision with the first x) but also the first x is not displayed, because it does not occur...

Pierre-Marie Pédrot (Apr 03 2017 at 18:26):

@Maxime Dénès The bench did not use the right branch for mathcomp :/

Maxime Dénès (Apr 03 2017 at 21:00):

@Enrico Tassi Yeah, we saw this one together some time ago. That's what I dub paranoid renaming.

Maxime Dénès (Apr 03 2017 at 21:01):

@Pierre-Marie Pédrot Yeah, we're waiting for support for overlays from @Matej Košík :)

Matej Košík (Gitter import) (Apr 03 2017 at 21:01):

@Maxime Dénès Tomorrow I'll try to implement them.

Maxime Dénès (Apr 03 2017 at 21:02):

Great! We can discuss it a bit, it requires a bit of design.

Matej Košík (Gitter import) (Apr 03 2017 at 21:02):

For today's job, I modified the script on pendulum to add the extra repository you have placed there. There are custom packages for coq-ssreflect.

Maxime Dénès (Apr 03 2017 at 21:03):

oh ok, thanks! So that's what Jenkin's \#26 is doing?

Matej Košík (Gitter import) (Apr 03 2017 at 21:03):

Yes.

Maxime Dénès (Apr 03 2017 at 21:04):

Sounds very good, thanks.

Maxime Dénès (Apr 03 2017 at 21:04):

@Pierre-Marie Pédrot What do you think of HoTT's timings?

Pierre-Marie Pédrot (Apr 03 2017 at 21:05):

They look OK.

Matej Košík (Gitter import) (Apr 03 2017 at 21:05):

The previous job worked itself as far as coq-mathcomp-ssreflect and then it crashed.
The intermediate results (from before the crash):

┌─────────────────┬─────────────────────────┬─────────────────────────────────────┬───────────────────────────────────────┐
│                 │      user time [s]      │             CPU cycles              │           CPU instructions            │
│                 │                         │                                     │                                       │
│    package_name │     NEW     OLD PDIFF   │           NEW           OLD PDIFF   │            NEW            OLD PDIFF   │
├─────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┤
│       coq-color │  631.49  650.80 -2.97 % │ 1754004131981 1803179944513 -2.73 % │  2205655960449  2339989943536 -5.74 % │
├─────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┤
│       coq-flocq │   55.58   55.59 -0.02 % │  152473845088  151365590486 +0.73 % │   194772860066   195218732996 -0.23 % │
├─────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┤
│ coq-fiat-crypto │ 2393.69 2371.60 +0.93 % │ 6651126154562 6595511506108 +0.84 % │ 10973828256053 10998944800258 -0.23 % │
├─────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┤
│          coq-sf │   45.96   45.47 +1.08 % │  125554592434  124037099135 +1.22 % │   164277938151   163715060784 +0.34 % │
├─────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┤
│     coq-unimath │ 1285.03 1258.59 +2.10 % │ 3563758045063 3492057761063 +2.05 % │  5942466363507  5849766688064 +1.58 % │
├─────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┤
│        coq-hott │  239.56  230.82 +3.79 % │  646887985092  621646051095 +4.06 % │  1095798838565  1050349361476 +4.33 % │
└─────────────────┴─────────────────────────┴─────────────────────────────────────┴───────────────────────────────────────┘

Pierre-Marie Pédrot (Apr 03 2017 at 21:05):

I think we're close to merging EConstr, aren't we?

Matej Košík (Gitter import) (Apr 03 2017 at 21:05):

I fixed the reasons why the script was crashing (it was a bug I introduced today :-( )

Matej Košík (Gitter import) (Apr 03 2017 at 21:06):

(but anyway, without those "overlays" wouldn't provide more results)

Maxime Dénès (Apr 03 2017 at 21:06):

I think we are getting close, yes. Still not ideal because we are above 2% overhead.

Maxime Dénès (Apr 03 2017 at 21:06):

You'll need to convince everyone ;)

Pierre-Marie Pédrot (Apr 03 2017 at 21:07):

Come on, that's coq-hott.

Maxime Dénès (Apr 03 2017 at 21:07):

You should draw a chart performance x correctness

Pierre-Marie Pédrot (Apr 03 2017 at 21:08):

We need an axis about program proof...

Pierre-Marie Pédrot (Apr 03 2017 at 21:08):

It's possible to have full performance at the expanse of proving your code!

Maxime Dénès (Apr 03 2017 at 21:08):

Proofs are overrated.

Pierre-Marie Pédrot (Apr 03 2017 at 21:09):

The good thing is that if we track all the unsafe casts, it'll become possible to use a dedicated datastructure for EConstr.t

Maxime Dénès (Apr 03 2017 at 21:09):

WDYM?

Pierre-Marie Pédrot (Apr 03 2017 at 21:09):

For instance, some kind of imperative but persistent representation.

Maxime Dénès (Apr 03 2017 at 21:09):

oh yes

Maxime Dénès (Apr 03 2017 at 21:10):

didn't they use to have that in like Coq 4?

Pierre-Marie Pédrot (Apr 03 2017 at 21:10):

So that one does evar normalization literally only once.

Pierre-Marie Pédrot (Apr 03 2017 at 21:10):

No idea, I can have a look

Maxime Dénès (Apr 03 2017 at 21:10):

Maybe it was not for evar or meta substitution

Pierre-Marie Pédrot (Apr 03 2017 at 21:10):

that'd be @Emilio Jesús Gallego Arias's sweet dream

Maxime Dénès (Apr 03 2017 at 21:10):

but I've heard one day about an imperative data structure for Coq terms

Maxime Dénès (Apr 03 2017 at 21:11):

don't know if it was a legend

Pierre-Marie Pédrot (Apr 03 2017 at 21:11):

Coq source code. A time of legend and heroes

Maxime Dénès (Apr 03 2017 at 21:11):

That would make a great movie.

Pierre-Marie Pédrot (Apr 03 2017 at 21:11):

a horror movie most probably

Matej Košík (Gitter import) (Apr 03 2017 at 21:11):

@Maxime Dénès That special ssreflect OPAM packages are needed for both commits?

Maxime Dénès (Apr 03 2017 at 21:12):

nope, not for trunk

Matej Košík (Gitter import) (Apr 03 2017 at 21:13):

Hmmm. The job has failed again when trying to compile coq-mathcomp-ssreflect, as if it pulled again the wrong version of it....

Maxime Dénès (Apr 03 2017 at 21:13):

oh no, that's a different one

Maxime Dénès (Apr 03 2017 at 21:14):

We need the custom package for head but not for base. Is it what you did?

Matej Košík (Gitter import) (Apr 03 2017 at 21:16):

That's what I tried, but could easily made a mistake.
I will tomorrow start with compiling coq-mathcomp-ssreflect manually (with Econstrified Coq).
When that works, it will be obvious how to update the script.

Matej Košík (Gitter import) (Apr 03 2017 at 21:16):

Anyway, you can see my modification on pendulum...

Maxime Dénès (Apr 03 2017 at 21:18):

Yeah you added the repo instead of replacing it...

Matej Košík (Gitter import) (Apr 03 2017 at 21:20):

The repo-list looks all-right:

  50 [local] opam-coq-archive     /home/jenkins/git/coq-bench/opam-coq-archive
  40 [local]  coq-bench     /home/jenkins/git/coq-bench/opam
  30 [http]  coq-released     https://coq.inria.fr/opam/released
  20 [http]  coq-extra-dev     https://coq.inria.fr/opam/extra-dev
  10 [local] custom-opam-repo     /home/jenkins/workspace/benchmark-part-of-the-branch/26/custom_opam_repo
   0 [http]     default     https://opam.ocaml.org

I'll start tomorrow by debugging why this did not work.

Matej Košík (Gitter import) (Apr 03 2017 at 21:21):

Btw. do I understand it correctly that in opam-coq-archive you do not actually need all that stuff?

Maxime Dénès (Apr 03 2017 at 21:22):

It doesn't work because it fetches mathcomp from coq-extra-dev.

Matej Košík (Gitter import) (Apr 03 2017 at 21:22):

The numbers on the left are priorities? The lower the number, the higher the priority?

Maxime Dénès (Apr 03 2017 at 21:23):

I don't know, but why keep coq-extra-dev?

Maxime Dénès (Apr 03 2017 at 21:25):

I adjusted it.

Maxime Dénès (Apr 03 2017 at 21:25):

Can you launch a last one?

Maxime Dénès (Apr 03 2017 at 21:25):

Maybe it will run over night this time.

Matej Košík (Gitter import) (Apr 03 2017 at 21:25):

Done. Let's see...

Maxime Dénès (Apr 03 2017 at 21:29):

I saw you solved the issues, sounds very good.

Matej Košík (Gitter import) (Apr 03 2017 at 21:36):

Thanks. Tomorrow I can try to tackle overlays. That sounds useful. Then we may decide. Many things remain:

The embarrassing (but not painful in practise) limitation of topological sort.
Highly painful duplication of data between Travis/Jenkins.
...

Maxime Dénès (Apr 03 2017 at 22:19):

@Matej Košík git show 4f041384cb27f0d24fa14b272884b4b7f69cacbe kernel/nativecode.ml

Matej Košík (Gitter import) (Apr 03 2017 at 22:20):

Maxime Dénès (Apr 03 2017 at 22:21):

and compile_rel env sigma univ auxdefs n =
-  let decl = Context.Rel.lookup n env.env_rel_context in
-  let n = Context.Rel.length env.env_rel_context - n in
-  let open Context.Rel.Declaration in
-  match decl with
+  let open Context.Rel in
+  let n = length env.env_rel_context - n in
+  let open Declaration in
+  match lookup n env.env_rel_context with

Pierre-Marie Pédrot (Apr 03 2017 at 22:22):

Shitstorm in approach!

Maxime Dénès (Apr 03 2017 at 22:22):

That's what causes https://coq.inria.fr/bugs/show_bug.cgi?id=5435

Maxime Dénès (Apr 03 2017 at 22:23):

So? Any player?

Maxime Dénès (Apr 03 2017 at 22:24):

hint: the first let-in was there for a reason

Maxime Dénès (Apr 03 2017 at 22:25):

let's make it a proof of false

Pierre-Marie Pédrot (Apr 03 2017 at 22:25):

I'm currently myself looking at the way we handle universe constraints in the kernel.

Pierre-Marie Pédrot (Apr 03 2017 at 22:26):

There are suspicious discrepancies.

Maxime Dénès (Apr 03 2017 at 22:26):

I wouldn't be surprised...

Pierre-Marie Pédrot (Apr 03 2017 at 22:26):

Actually I'm hoping to give static invariants to it

Pierre-Marie Pédrot (Apr 03 2017 at 22:26):

by carefully chosing datatypes, and encoding info in GADTs

Maxime Dénès (Apr 03 2017 at 22:26):

@Pierre-Marie Pédrot, what goes in env_rel_context? Do section let-ins go there?

Pierre-Marie Pédrot (Apr 03 2017 at 22:26):

nah

Maxime Dénès (Apr 03 2017 at 22:27):

hmmm

Pierre-Marie Pédrot (Apr 03 2017 at 22:27):

You need to be inside a term for it to be non-empty.

Pierre-Marie Pédrot (Apr 03 2017 at 22:27):

I think.

Maxime Dénès (Apr 03 2017 at 22:27):

yeah but fortunately I have native casts

Pierre-Marie Pédrot (Apr 03 2017 at 22:27):

\o/

Pierre-Marie Pédrot (Apr 03 2017 at 22:27):

Fortunately.

Pierre-Marie Pédrot (Apr 03 2017 at 22:28):

That's what you get for trusting native_compute.

Maxime Dénès (Apr 03 2017 at 22:29):

Well, I'm surprised that the same kind of "refactoring" wasn't done on the VM ;)

Pierre-Marie Pédrot (Apr 03 2017 at 22:29):

What about my PR touching the kernel btw?

Pierre-Marie Pédrot (Apr 03 2017 at 22:30):

I'm pushing for the swift integration of the array mapping one !

Maxime Dénès (Apr 03 2017 at 22:31):

Was there any complaint?

Maxime Dénès (Apr 03 2017 at 22:31):

I'll read again

Pierre-Marie Pédrot (Apr 03 2017 at 22:31):

I think @silene complained about the ugliness.

Maxime Dénès (Apr 03 2017 at 22:31):

Let me finish my proof of false. I put too many assertions...

Pierre-Marie Pédrot (Apr 03 2017 at 23:01):

So, is Coq 8.6 inconsistent?

Maxime Dénès (Apr 03 2017 at 23:11):

Hmm I don't understand why my term doesn't type check

Maxime Dénès (Apr 03 2017 at 23:11):

Maybe you can help me:

Maxime Dénès (Apr 03 2017 at 23:11):

Definition foo (T := False) (U := T) (x : True) (X := True) := x <<: U.

Pierre-Marie Pédrot (Apr 03 2017 at 23:11):

Lemme see

Maxime Dénès (Apr 03 2017 at 23:12):

How does the typechecker know I'm trying to make fun of him?

Pierre-Marie Pédrot (Apr 03 2017 at 23:12):

He's reached self-consciousness

Maxime Dénès (Apr 03 2017 at 23:12):

try e.g. Definition foo (T := False) (U := T) (x : True) (X := True) := Eval native_compute in U.

Maxime Dénès (Apr 03 2017 at 23:13):

In fact, when I use the cast, two type checks are triggered

Maxime Dénès (Apr 03 2017 at 23:13):

the first one is nice and buggy, and succeeds, but the second compares True and False. So of course it fails.

Maxime Dénès (Apr 03 2017 at 23:13):

I don't understand where this second check comes from.

Pierre-Marie Pédrot (Apr 03 2017 at 23:14):

backtraces to the rescue!

Maxime Dénès (Apr 03 2017 at 23:15):

Yeah I looked at it already.

Pierre-Marie Pédrot (Apr 03 2017 at 23:18):

I get fancy assertion failures if I play a bit with the term.

Pierre-Marie Pédrot (Apr 03 2017 at 23:18):

We're walking on thin ice!

Maxime Dénès (Apr 03 2017 at 23:18):

Yeah but those are "expected" given the bug.

Maxime Dénès (Apr 03 2017 at 23:19):

But why are there two tests? And where does the typechecker see True and False without going through native_compute?

Pierre-Marie Pédrot (Apr 03 2017 at 23:21):

Interesting:

Pierre-Marie Pédrot (Apr 03 2017 at 23:22):

Definition foo (T := False) (U := T) (V := U) (x : True) (X := True) : V = False := (@eq_refl Prop U <<: @eq Prop V U).
In environment
T := False : Prop
x : True
X := True : Prop
The term "@eq_refl Prop T" has type "@eq Prop T T"
while it is expected to have type "@eq Prop T T".

Maxime Dénès (Apr 03 2017 at 23:23):

I don't understand how definitions are type checked...

Pierre-Marie Pédrot (Apr 03 2017 at 23:24):

I also get a few stack overflows

Maxime Dénès (Apr 03 2017 at 23:25):

did you make sense of the backtrace on my initial example?

Pierre-Marie Pédrot (Apr 03 2017 at 23:25):

Not quite, I'm launching a debugger to see what happens

Maxime Dénès (Apr 03 2017 at 23:26):

the other errors you see are probably at reification time

Maxime Dénès (Apr 03 2017 at 23:26):

but my example is cooked up to make the thing go through

Pierre-Marie Pédrot (Apr 03 2017 at 23:26):

All right.

Maxime Dénès (Apr 03 2017 at 23:27):

how do we go from term_typing to fast_typeops?

Pierre-Marie Pédrot (Apr 03 2017 at 23:28):

I think I got it.

Maxime Dénès (Apr 03 2017 at 23:28):

tell me :)

Pierre-Marie Pédrot (Apr 03 2017 at 23:28):

is native compilation enabled by default ?

Pierre-Marie Pédrot (Apr 03 2017 at 23:28):

I think not

Pierre-Marie Pédrot (Apr 03 2017 at 23:28):

it falls back to VM right?

Maxime Dénès (Apr 03 2017 at 23:28):

Yes it is enabled by default.

Pierre-Marie Pédrot (Apr 03 2017 at 23:28):

sure ?

Maxime Dénès (Apr 03 2017 at 23:29):

Sure. What is not enabled is the precompilation except for stdlib.

Maxime Dénès (Apr 03 2017 at 23:29):

And tests are running, I saw the generated code.

Pierre-Marie Pédrot (Apr 03 2017 at 23:29):

cause the native conversion fails in the cast

Maxime Dénès (Apr 03 2017 at 23:29):

From what I saw, it is called twice.

Maxime Dénès (Apr 03 2017 at 23:29):

The first time it succeeds, the second time it fails.

Pierre-Marie Pédrot (Apr 03 2017 at 23:30):

yep

Pierre-Marie Pédrot (Apr 03 2017 at 23:30):

same behaviour here

Maxime Dénès (Apr 03 2017 at 23:30):

But I don't understand the second call.

Maxime Dénès (Apr 03 2017 at 23:30):

Also, why don't we see something related to native_compute in the backtrace?

Pierre-Marie Pédrot (Apr 03 2017 at 23:30):

nah, that's because the trace is not propagated

Maxime Dénès (Apr 03 2017 at 23:31):

What does that mean? I'm always confused when trying to debug.

Maxime Dénès (Apr 03 2017 at 23:31):

Where is it not propagated?

Pierre-Marie Pédrot (Apr 03 2017 at 23:31):

one need to add some CErrors.push to Typeops.check_cast

Maxime Dénès (Apr 03 2017 at 23:32):

check_cast?!

Pierre-Marie Pédrot (Apr 03 2017 at 23:32):

yep

Maxime Dénès (Apr 03 2017 at 23:32):

There is no check_cast in 8.6.

Pierre-Marie Pédrot (Apr 03 2017 at 23:32):

oh, I'm on trunk

Pierre-Marie Pédrot (Apr 03 2017 at 23:32):

but that should be the same

Pierre-Marie Pédrot (Apr 03 2017 at 23:33):

The hell are we doing in the stm

Pierre-Marie Pédrot (Apr 03 2017 at 23:34):

something is wrong

Maxime Dénès (Apr 03 2017 at 23:34):

yeah I don't understand

Pierre-Marie Pédrot (Apr 03 2017 at 23:34):

it fails here

66     | Aind (ind1,u1), Aind (ind2,u2) ->
67        if eq_ind ind1 ind2 then convert_instances ~flex:false u1 u2 cu
68        else raise NotConvertible<|a|>

Maxime Dénès (Apr 03 2017 at 23:35):

the second time?

Maxime Dénès (Apr 03 2017 at 23:35):

yeah of course

Maxime Dénès (Apr 03 2017 at 23:35):

it's being asked to compare True and False

Pierre-Marie Pédrot (Apr 03 2017 at 23:35):

obviously

Maxime Dénès (Apr 03 2017 at 23:35):

but the question is who called it?

Maxime Dénès (Apr 03 2017 at 23:36):

I may be blind, but I don't see what typing rule does that.

Maxime Dénès (Apr 03 2017 at 23:36):

Except if somehow, we said that the type of x <<: T was the type of x...

Pierre-Marie Pédrot (Apr 03 2017 at 23:36):

so the native compiler is asked to compare

Pierre-Marie Pédrot (Apr 03 2017 at 23:36):

t1: Term.constr =
  let T := False in let U := T in fun _ : True => let X := True in True
t2: Term.constr =
  let T := False in let U := T in fun _ : True => let X := True in U

Maxime Dénès (Apr 03 2017 at 23:37):

Ah yeah

Maxime Dénès (Apr 03 2017 at 23:37):

Where are the casts gone?!

Pierre-Marie Pédrot (Apr 03 2017 at 23:38):

no, we're checking the cast

Maxime Dénès (Apr 03 2017 at 23:38):

Oh!

Pierre-Marie Pédrot (Apr 03 2017 at 23:38):

isn't that supposed to be the same because of your bug?

Maxime Dénès (Apr 03 2017 at 23:38):

Well it depends. I thought what we were doing

Pierre-Marie Pédrot (Apr 03 2017 at 23:39):

Erm...

Pierre-Marie Pédrot (Apr 03 2017 at 23:39):

isn't that because of this implementation ?

Maxime Dénès (Apr 03 2017 at 23:39):

was asking to compare True and U in the rel_context that corresponds to what you wrote.

Pierre-Marie Pédrot (Apr 03 2017 at 23:39):

let native_conv cv_pb sigma env t1 t2 =
  if Coq_config.no_native_compiler then begin
    warn_no_native_compiler ();
    vm_conv cv_pb env t1 t2
  end
  else
  let univs = Environ.universes env in
  let b =
    if cv_pb = CUMUL then Constr.leq_constr_univs univs t1 t2
    else Constr.eq_constr_univs univs t1 t2
  in
  if not b then
    let univs = (univs, checked_universes) in
    let t1 = Term.it_mkLambda_or_LetIn t1 (Environ.rel_context env) in
    let t2 = Term.it_mkLambda_or_LetIn t2 (Environ.rel_context env) in
    let _ = native_conv_gen cv_pb sigma env univs t1 t2 in ()

Maxime Dénès (Apr 03 2017 at 23:39):

hum

Pierre-Marie Pédrot (Apr 03 2017 at 23:39):

we abstract over the context

Maxime Dénès (Apr 03 2017 at 23:39):

I'm too paranoid.

Pierre-Marie Pédrot (Apr 03 2017 at 23:40):

so, no soundness bug?

Maxime Dénès (Apr 03 2017 at 23:40):

But then who makes the first call?

Pierre-Marie Pédrot (Apr 03 2017 at 23:40):

the environment is wrong that said

Maxime Dénès (Apr 03 2017 at 23:41):

The first call produces wrong code, I checked.

Pierre-Marie Pédrot (Apr 03 2017 at 23:41):

Nah, in trunk there is only one call which is NativeCast

Maxime Dénès (Apr 03 2017 at 23:41):

Yeah but probably there is one in the pretyper.

Maxime Dénès (Apr 03 2017 at 23:41):

I got it know.

Pierre-Marie Pédrot (Apr 03 2017 at 23:41):

Maxime Dénès (Apr 03 2017 at 23:41):

Hum not quite.

Maxime Dénès (Apr 03 2017 at 23:42):

In 8.6, I can swear the compiler is called at least twice.

Maxime Dénès (Apr 03 2017 at 23:42):

I see the generated code.

Pierre-Marie Pédrot (Apr 03 2017 at 23:42):

I can check if you want

Maxime Dénès (Apr 03 2017 at 23:42):

The first time it is incorrect, the second time it is correct.

Pierre-Marie Pédrot (Apr 03 2017 at 23:43):

clearly the code has changed between trunk and 8.6

Maxime Dénès (Apr 03 2017 at 23:43):

let me try in trunk

Maxime Dénès (Apr 03 2017 at 23:44):

still two calls

Maxime Dénès (Apr 03 2017 at 23:44):

probably with different environments

Pierre-Marie Pédrot (Apr 03 2017 at 23:45):

can't reproduce on trunk

Maxime Dénès (Apr 03 2017 at 23:45):

if you do -debug

Maxime Dénès (Apr 03 2017 at 23:45):

you can look for .native files in /tmp

Pierre-Marie Pédrot (Apr 03 2017 at 23:45):

I'm in the debugger, this does not work

Pierre-Marie Pédrot (Apr 03 2017 at 23:46):

nah, in 8.6 only one native cast as well

Pierre-Marie Pédrot (Apr 03 2017 at 23:46):

I'm using bytecode so I'm not sure what is supposed to happen

Pierre-Marie Pédrot (Apr 03 2017 at 23:47):

still, isn't because you abstract over the term that it does not break loose?

Maxime Dénès (Apr 03 2017 at 23:47):

probably

Maxime Dénès (Apr 03 2017 at 23:48):

can you try in native?

Maxime Dénès (Apr 03 2017 at 23:48):

so what you get in /tmp

Maxime Dénès (Apr 03 2017 at 23:48):

see*

Pierre-Marie Pédrot (Apr 03 2017 at 23:48):

lemme try

Maxime Dénès (Apr 03 2017 at 23:48):

I'd like to understand why there are two calls, because maybe we are inefficient

Maxime Dénès (Apr 03 2017 at 23:48):

independently of the soundness

Pierre-Marie Pédrot (Apr 03 2017 at 23:48):

What should I observe?

Pierre-Marie Pédrot (Apr 03 2017 at 23:48):

I can observe the backtrace if you want

Maxime Dénès (Apr 03 2017 at 23:49):

each conversion test leaves a xxxxx.nativefile in /tmp

Maxime Dénès (Apr 03 2017 at 23:49):

my example creates at least two on my machine

Maxime Dénès (Apr 03 2017 at 23:49):

you can open them, they are ml source files

Maxime Dénès (Apr 03 2017 at 23:50):

what I see is the first is not abstracted over the context, but the second is

Pierre-Marie Pédrot (Apr 03 2017 at 23:50):

I'll tell you right now

Pierre-Marie Pédrot (Apr 03 2017 at 23:50):

I only get one call to nativeconv

Maxime Dénès (Apr 03 2017 at 23:50):

and you see only one file?

Pierre-Marie Pédrot (Apr 03 2017 at 23:51):

I get two

Maxime Dénès (Apr 03 2017 at 23:51):

WTF did I mess up?

Pierre-Marie Pédrot (Apr 03 2017 at 23:51):

no wait

Pierre-Marie Pédrot (Apr 03 2017 at 23:51):

I get none actually

Pierre-Marie Pédrot (Apr 03 2017 at 23:51):

there is indeed a compiled cmxs / o whatever

Maxime Dénès (Apr 03 2017 at 23:51):

if you don't put -debug, they don't stay

Pierre-Marie Pédrot (Apr 03 2017 at 23:52):

but no native

Pierre-Marie Pédrot (Apr 03 2017 at 23:52):

ah ok

Pierre-Marie Pédrot (Apr 03 2017 at 23:52):

in debug mode, I do get two calls to native compilation

Pierre-Marie Pédrot (Apr 03 2017 at 23:52):

and thus two files !

Maxime Dénès (Apr 03 2017 at 23:52):

what?!?!

Pierre-Marie Pédrot (Apr 03 2017 at 23:52):

isn't that some stm story?

Maxime Dénès (Apr 03 2017 at 23:52):

only in debug mode?

Pierre-Marie Pédrot (Apr 03 2017 at 23:52):

about backtrack blahblah

Pierre-Marie Pédrot (Apr 03 2017 at 23:52):

yep

Maxime Dénès (Apr 03 2017 at 23:53):

but it's not even the same environment

Pierre-Marie Pédrot (Apr 03 2017 at 23:53):

who knows

Maxime Dénès (Apr 03 2017 at 23:53):

something bad is going on

Pierre-Marie Pédrot (Apr 03 2017 at 23:53):

First backtrace:

Pierre-Marie Pédrot (Apr 03 2017 at 23:53):

======
Raised by primitive operation at file "kernel/nativeconv.ml", line 158, characters 11-41
Called from file "kernel/fast_typeops.ml", line 233, characters 6-61
Called from file "kernel/fast_typeops.ml", line 396, characters 14-40
Called from file "kernel/fast_typeops.ml", line 390, characters 16-31
Called from file "kernel/fast_typeops.ml", line 376, characters 16-31
Called from file "kernel/fast_typeops.ml", line 390, characters 16-31
Called from file "kernel/fast_typeops.ml", line 390, characters 16-31
Called from file "kernel/fast_typeops.ml", line 449, characters 10-28
Called from file "kernel/fast_typeops.ml" (inlined), line 456, characters 19-28
Called from file "kernel/term_typing.ml", line 250, characters 14-28
Called from file "kernel/term_typing.ml" (inlined), line 414, characters 4-50
Called from file "kernel/safe_typing.ml", line 525, characters 8-68
Called from file "library/global.ml", line 68, characters 16-31
Called from file "library/declare.ml", line 155, characters 26-65
Called from file "library/lib.ml", line 215, characters 2-26
Called from file "library/declare.ml", line 215, characters 23-36
Called from file "library/declare.ml", line 269, characters 11-41
Called from file "toplevel/command.ml", line 158, characters 11-77
Called from file "toplevel/command.ml", line 190, characters 4-54
Called from file "toplevel/command.ml", line 218, characters 12-145
Called from file "lib/flags.ml", line 11, characters 15-18
Called from file "lib/flags.ml" (inlined), line 150, characters 19-41
Called from file "toplevel/vernacentries.ml", line 2235, characters 17-69
Called from file "toplevel/vernacentries.ml", line 2232, characters 10-389
Called from file "stm/stm.ml", line 122, characters 15-71
Called from file "stm/stm.ml", line 2143, characters 10-28
Called from file "stm/stm.ml", line 885, characters 6-10
Called from file "stm/stm.ml", line 2258, characters 4-100
Called from file "stm/stm.ml", line 2291, characters 4-48
Called from file "stm/stm.ml", line 2301, characters 2-35
Called from file "stm/stm.ml", line 2831, characters 8-30
Called from file "toplevel/vernac.ml", line 203, characters 6-16
Called from file "lib/flags.ml", line 11, characters 15-18
Called from file "lib/flags.ml" (inlined), line 150, characters 19-41
Called from file "toplevel/vernac.ml", line 221, characters 6-87
Called from file "toplevel/vernac.ml", line 311, characters 14-48
Called from file "toplevel/vernac.ml", line 348, characters 2-13
Called from file "list.ml", line 77, characters 12-15
Called from file "toplevel/coqtop.ml", line 640, characters 6-22
Called from file "toplevel/coqtop.ml", line 664, characters 11-59
Called from file "/tmp/coqmain5bd0d9.ml", line 2, characters 17-31
======

Pierre-Marie Pédrot (Apr 03 2017 at 23:53):

argh no

Pierre-Marie Pédrot (Apr 03 2017 at 23:54):

that's the backtrace of the error sorry

Pierre-Marie Pédrot (Apr 03 2017 at 23:54):

but I do get two files

Pierre-Marie Pédrot (Apr 03 2017 at 23:54):

strace to the rescue

Maxime Dénès (Apr 03 2017 at 23:54):

so maybe that is independent from the debug mode, right?

Maxime Dénès (Apr 03 2017 at 23:55):

I have a feeling I screwed up something myself here ^^

Pierre-Marie Pédrot (Apr 03 2017 at 23:55):

Yeah, right, I get 2 cmxs even without debug

Maxime Dénès (Apr 03 2017 at 23:55):

but I have no idea what

Pierre-Marie Pédrot (Apr 03 2017 at 23:55):

I can look at who opens a file

Maxime Dénès (Apr 03 2017 at 23:56):

well

Maxime Dénès (Apr 03 2017 at 23:56):

it is native_conv

Maxime Dénès (Apr 03 2017 at 23:56):

so the only missing bit is to find the two calls

Pierre-Marie Pédrot (Apr 03 2017 at 23:56):

no, I'd see the other trace

Pierre-Marie Pédrot (Apr 03 2017 at 23:56):

at least it's not Nativeconv.native_conv

Pierre-Marie Pédrot (Apr 03 2017 at 23:56):

maybe native_conv_gen, let me check

Maxime Dénès (Apr 03 2017 at 23:56):

native_conv_gen?

Maxime Dénès (Apr 03 2017 at 23:56):

yeah

Maxime Dénès (Apr 03 2017 at 23:57):

it would explain why it's not abstracted...

Maxime Dénès (Apr 03 2017 at 23:57):

this part is terrible, I'm ashamed

Pierre-Marie Pédrot (Apr 03 2017 at 23:57):

indeed

Maxime Dénès (Apr 03 2017 at 23:57):

"used outside of the kernel"

Maxime Dénès (Apr 03 2017 at 23:57):

says the comment :)

Pierre-Marie Pédrot (Apr 03 2017 at 23:57):

Here are the backtraces

======
Raised by primitive operation at file "kernel/nativeconv.ml", line 133, characters 11-41
Called from file "pretyping/reductionops.ml", line 1297, characters 3-73
Called from file "pretyping/pretyping.ml", line 1024, characters 21-83
Called from file "pretyping/pretyping.ml", line 1102, characters 8-72
Called from file "pretyping/pretyping.ml", line 1174, characters 17-77
Called from file "interp/constrintern.ml", line 2010, characters 4-52
Called from file "toplevel/command.ml", line 103, characters 16-64
Called from file "toplevel/command.ml", line 198, characters 4-56
Called from file "lib/flags.ml", line 11, characters 15-18
Called from file "lib/flags.ml" (inlined), line 150, characters 19-41
Called from file "toplevel/vernacentries.ml", line 2235, characters 17-69
Called from file "toplevel/vernacentries.ml", line 2232, characters 10-389
Called from file "stm/stm.ml", line 122, characters 15-71
Called from file "stm/stm.ml", line 2143, characters 10-28
Called from file "stm/stm.ml", line 885, characters 6-10
Called from file "stm/stm.ml", line 2258, characters 4-100
Called from file "stm/stm.ml", line 2291, characters 4-48
Called from file "stm/stm.ml", line 2301, characters 2-35
Called from file "stm/stm.ml", line 2831, characters 8-30
Called from file "toplevel/vernac.ml", line 203, characters 6-16
Called from file "lib/flags.ml", line 11, characters 15-18
Called from file "lib/flags.ml" (inlined), line 150, characters 19-41
Called from file "toplevel/vernac.ml", line 221, characters 6-87
Called from file "toplevel/vernac.ml", line 311, characters 14-48
Called from file "toplevel/vernac.ml", line 348, characters 2-13
Called from file "list.ml", line 77, characters 12-15
Called from file "toplevel/coqtop.ml", line 640, characters 6-22
Called from file "toplevel/coqtop.ml", line 664, characters 11-59
Called from file "/tmp/coqmain79e4c9.ml", line 2, characters 17-31
======
======
Raised by primitive operation at file "kernel/nativeconv.ml", line 133, characters 11-41
Called from file "kernel/nativeconv.ml", line 175, characters 12-55
Called from file "kernel/fast_typeops.ml", line 233, characters 6-61
Called from file "kernel/fast_typeops.ml", line 396, characters 14-40
Called from file "kernel/fast_typeops.ml", line 390, characters 16-31
Called from file "kernel/fast_typeops.ml", line 376, characters 16-31
Called from file "kernel/fast_typeops.ml", line 390, characters 16-31
Called from file "kernel/fast_typeops.ml", line 390, characters 16-31
Called from file "kernel/fast_typeops.ml", line 449, characters 10-28
Called from file "kernel/fast_typeops.ml" (inlined), line 456, characters 19-28
Called from file "kernel/term_typing.ml", line 250, characters 14-28
Called from file "kernel/term_typing.ml" (inlined), line 414, characters 4-50
Called from file "kernel/safe_typing.ml", line 525, characters 8-68
Called from file "library/global.ml", line 68, characters 16-31
Called from file "library/declare.ml", line 155, characters 26-65
Called from file "library/lib.ml", line 215, characters 2-26
Called from file "library/declare.ml", line 215, characters 23-36
Called from file "library/declare.ml", line 269, characters 11-41
Called from file "toplevel/command.ml", line 158, characters 11-77
Called from file "toplevel/command.ml", line 190, characters 4-54
Called from file "toplevel/command.ml", line 218, characters 12-145
Called from file "lib/flags.ml", line 11, characters 15-18
Called from file "lib/flags.ml" (inlined), line 150, characters 19-41
Called from file "toplevel/vernacentries.ml", line 2235, characters 17-69
Called from file "toplevel/vernacentries.ml", line 2232, characters 10-389
Called from file "stm/stm.ml", line 122, characters 15-71
Called from file "stm/stm.ml", line 2143, characters 10-28
Called from file "stm/stm.ml", line 885, characters 6-10
Called from file "stm/stm.ml", line 2258, characters 4-100
Called from file "stm/stm.ml", line 2291, characters 4-48
Called from file "stm/stm.ml", line 2301, characters 2-35
Called from file "stm/stm.ml", line 2831, character

Pierre-Marie Pédrot (Apr 03 2017 at 23:57):

Rhat

Pierre-Marie Pédrot (Apr 03 2017 at 23:57):

it does not fit

Pierre-Marie Pédrot (Apr 03 2017 at 23:57):

let's split them

Pierre-Marie Pédrot (Apr 03 2017 at 23:58):

Raised by primitive operation at file "kernel/nativeconv.ml", line 133, characters 11-41
Called from file "pretyping/reductionops.ml", line 1297, characters 3-73
Called from file "pretyping/pretyping.ml", line 1024, characters 21-83
Called from file "pretyping/pretyping.ml", line 1102, characters 8-72
Called from file "pretyping/pretyping.ml", line 1174, characters 17-77
Called from file "interp/constrintern.ml", line 2010, characters 4-52
Called from file "toplevel/command.ml", line 103, characters 16-64
Called from file "toplevel/command.ml", line 198, characters 4-56
Called from file "lib/flags.ml", line 11, characters 15-18
Called from file "lib/flags.ml" (inlined), line 150, characters 19-41
Called from file "toplevel/vernacentries.ml", line 2235, characters 17-69
Called from file "toplevel/vernacentries.ml", line 2232, characters 10-389
Called from file "stm/stm.ml", line 122, characters 15-71
Called from file "stm/stm.ml", line 2143, characters 10-28
Called from file "stm/stm.ml", line 885, characters 6-10
Called from file "stm/stm.ml", line 2258, characters 4-100
Called from file "stm/stm.ml", line 2291, characters 4-48
Called from file "stm/stm.ml", line 2301, characters 2-35
Called from file "stm/stm.ml", line 2831, characters 8-30
Called from file "toplevel/vernac.ml", line 203, characters 6-16
Called from file "lib/flags.ml", line 11, characters 15-18
Called from file "lib/flags.ml" (inlined), line 150, characters 19-41
Called from file "toplevel/vernac.ml", line 221, characters 6-87
Called from file "toplevel/vernac.ml", line 311, characters 14-48
Called from file "toplevel/vernac.ml", line 348, characters 2-13
Called from file "list.ml", line 77, characters 12-15
Called from file "toplevel/coqtop.ml", line 640, characters 6-22
Called from file "toplevel/coqtop.ml", line 664, characters 11-59
Called from file "/tmp/coqmain79e4c9.ml", line 2, characters 17-31

Pierre-Marie Pédrot (Apr 03 2017 at 23:58):

Then

Pierre-Marie Pédrot (Apr 03 2017 at 23:58):

Raised by primitive operation at file "kernel/nativeconv.ml", line 133, characters 11-41
Called from file "kernel/nativeconv.ml", line 175, characters 12-55
Called from file "kernel/fast_typeops.ml", line 233, characters 6-61
Called from file "kernel/fast_typeops.ml", line 396, characters 14-40
Called from file "kernel/fast_typeops.ml", line 390, characters 16-31
Called from file "kernel/fast_typeops.ml", line 376, characters 16-31
Called from file "kernel/fast_typeops.ml", line 390, characters 16-31
Called from file "kernel/fast_typeops.ml", line 390, characters 16-31
Called from file "kernel/fast_typeops.ml", line 449, characters 10-28
Called from file "kernel/fast_typeops.ml" (inlined), line 456, characters 19-28
Called from file "kernel/term_typing.ml", line 250, characters 14-28
Called from file "kernel/term_typing.ml" (inlined), line 414, characters 4-50
Called from file "kernel/safe_typing.ml", line 525, characters 8-68
Called from file "library/global.ml", line 68, characters 16-31
Called from file "library/declare.ml", line 155, characters 26-65
Called from file "library/lib.ml", line 215, characters 2-26
Called from file "library/declare.ml", line 215, characters 23-36
Called from file "library/declare.ml", line 269, characters 11-41
Called from file "toplevel/command.ml", line 158, characters 11-77
Called from file "toplevel/command.ml", line 190, characters 4-54
Called from file "toplevel/command.ml", line 218, characters 12-145
Called from file "lib/flags.ml", line 11, characters 15-18
Called from file "lib/flags.ml" (inlined), line 150, characters 19-41
Called from file "toplevel/vernacentries.ml", line 2235, characters 17-69
Called from file "toplevel/vernacentries.ml", line 2232, characters 10-389
Called from file "stm/stm.ml", line 122, characters 15-71
Called from file "stm/stm.ml", line 2143, characters 10-28
Called from file "stm/stm.ml", line 885, characters 6-10
Called from file "stm/stm.ml", line 2258, characters 4-100
Called from file "stm/stm.ml", line 2291, characters 4-48
Called from file "stm/stm.ml", line 2301, characters 2-35
Called from file "stm/stm.ml", line 2831, characters 8-30
Called from file "toplevel/vernac.ml", line 203, characters 6-16
Called from file "lib/flags.ml", line 11, characters 15-18
Called from file "lib/flags.ml" (inlined), line 150, characters 19-41
Called from file "toplevel/vernac.ml", line 221, characters 6-87
Called from file "toplevel/vernac.ml", line 311, characters 14-48
Called from file "toplevel/vernac.ml", line 348, characters 2-13
Called from file "list.ml", line 77, characters 12-15
Called from file "toplevel/coqtop.ml", line 640, characters 6-22
Called from file "toplevel/coqtop.ml", line 664, characters 11-59
Called from file "/tmp/coqmain79e4c9.ml", line 2, characters 17-31

Maxime Dénès (Apr 03 2017 at 23:58):

yeah sorry, I understand now

Pierre-Marie Pédrot (Apr 03 2017 at 23:58):

so reductionops is calling it

Maxime Dénès (Apr 03 2017 at 23:58):

there is an infer_conv for native

Maxime Dénès (Apr 03 2017 at 23:59):

to infer univ constraints and so on

Pierre-Marie Pédrot (Apr 03 2017 at 23:59):

ah!

Maxime Dénès (Apr 03 2017 at 23:59):

I had forgotten about that

Maxime Dénès (Apr 03 2017 at 23:59):

before universes there was only one conv function

Maxime Dénès (Apr 03 2017 at 23:59):

and one for normalizing

Maxime Dénès (Apr 03 2017 at 23:59):

so we did learn one thing: the kernel function abstract over the context, but not the pretyper

Pierre-Marie Pédrot (Apr 04 2017 at 00:00):

yep !

Pierre-Marie Pédrot (Apr 04 2017 at 00:00):

once again, doubling everything saves the day

Maxime Dénès (Apr 04 2017 at 00:00):

it is probably more efficient to do it

Maxime Dénès (Apr 04 2017 at 00:00):

but I was scared to remove it from the kernel

Pierre-Marie Pédrot (Apr 04 2017 at 00:00):

well in that case the kernel was right

Pierre-Marie Pédrot (Apr 04 2017 at 00:00):

but just in case you never know

Maxime Dénès (Apr 04 2017 at 00:00):

I mean more efficient not to do it

Maxime Dénès (Apr 04 2017 at 00:00):

yeah

Pierre-Marie Pédrot (Apr 04 2017 at 00:00):

not that the passed environment is still wrong

Maxime Dénès (Apr 04 2017 at 00:00):

really?

Pierre-Marie Pédrot (Apr 04 2017 at 00:00):

I don't think there is a way to work around that

Pierre-Marie Pédrot (Apr 04 2017 at 00:01):

yes, if you abstract over it

Pierre-Marie Pédrot (Apr 04 2017 at 00:01):

you should clear the rel context

Maxime Dénès (Apr 04 2017 at 00:01):

oh yes

Pierre-Marie Pédrot (Apr 04 2017 at 00:01):

I don't think you can exploit that but still

Maxime Dénès (Apr 04 2017 at 00:01):

but it's unused then

Maxime Dénès (Apr 04 2017 at 00:01):

I agree it's not pretty

Pierre-Marie Pédrot (Apr 04 2017 at 00:01):

I'm always afraid about universe constraints

Maxime Dénès (Apr 04 2017 at 00:01):

also we compile a lot of useless stuff

Pierre-Marie Pédrot (Apr 04 2017 at 00:01):

couldn't you get a leak by duplicating the relcontext?

Maxime Dénès (Apr 04 2017 at 00:02):

I have no idea.

Pierre-Marie Pédrot (Apr 04 2017 at 00:02):

speaking about which, did you have a look at malfunction in the end?

Maxime Dénès (Apr 04 2017 at 00:02):

not that I remember

Maxime Dénès (Apr 04 2017 at 00:03):

did you talk to me about it? :)

Maxime Dénès (Apr 04 2017 at 00:03):

I forget things these days

Pierre-Marie Pédrot (Apr 04 2017 at 00:03):

yep I did !

Pierre-Marie Pédrot (Apr 04 2017 at 00:03):

that's just an API over dlambda

Pierre-Marie Pédrot (Apr 04 2017 at 00:03):

probably better than spitting Obj-ified ML code

Maxime Dénès (Apr 04 2017 at 00:03):

I see, that sounds nice.

Pierre-Marie Pédrot (Apr 04 2017 at 00:03):

since we're in OCaml 4.02...

Maxime Dénès (Apr 04 2017 at 00:04):

But how good is it to depend on it?

Pierre-Marie Pédrot (Apr 04 2017 at 00:04):

well, that's a very small wrapper

Pierre-Marie Pédrot (Apr 04 2017 at 00:04):

we could probably integrate it ourselves, but the advantage is that we deport compatiblity on a package

Pierre-Marie Pédrot (Apr 04 2017 at 00:04):

I'm not sure about how stable dlambda is

Maxime Dénès (Apr 04 2017 at 00:04):

Hum

Maxime Dénès (Apr 04 2017 at 00:04):

"Malfunction is released under the same terms as OCaml."

Pierre-Marie Pédrot (Apr 04 2017 at 00:04):

the subset you use is small

Pierre-Marie Pédrot (Apr 04 2017 at 00:05):

well, we could recode it

Maxime Dénès (Apr 04 2017 at 00:05):

oh but it's LGPL now?

Pierre-Marie Pédrot (Apr 04 2017 at 00:05):

yeah, how juridically clear is native_compute BTW ?

Maxime Dénès (Apr 04 2017 at 00:05):

it is very clear!

Maxime Dénès (Apr 04 2017 at 00:05):

much clearer than EConstr!

Pierre-Marie Pédrot (Apr 04 2017 at 00:05):

LGPL 2.1

Pierre-Marie Pédrot (Apr 04 2017 at 00:05):

what?

Pierre-Marie Pédrot (Apr 04 2017 at 00:06):

The Great Proud University of Ljubljana

Pierre-Marie Pédrot (Apr 04 2017 at 00:06):

has now shares in Coq

Pierre-Marie Pédrot (Apr 04 2017 at 00:06):

BEHOLD

Pierre-Marie Pédrot (Apr 04 2017 at 00:06):

First, American first lady

Pierre-Marie Pédrot (Apr 04 2017 at 00:06):

now: Coq

Maxime Dénès (Apr 04 2017 at 00:06):

now if you mean what happens if a plane crashes because of a wrong DeBruijn index in native_compute I'm not sure.

Pierre-Marie Pédrot (Apr 04 2017 at 00:07):

« c'est comme d'habitude : le gouvernement niera avoir eu connaissance... »

Pierre-Marie Pédrot (Apr 04 2017 at 00:07):

LGPL, dude

Pierre-Marie Pédrot (Apr 04 2017 at 00:07):

that's like we're gangsta

Pierre-Marie Pédrot (Apr 04 2017 at 00:07):

no liability whatsoever

Pierre-Marie Pédrot (Apr 04 2017 at 00:08):

still, I think it would be worthwile to plug directly into dlambda

Maxime Dénès (Apr 04 2017 at 00:08):

I'll give Matej's name :)

Maxime Dénès (Apr 04 2017 at 00:09):

what we should do is remove all this

Maxime Dénès (Apr 04 2017 at 00:09):

and implement Coqonut!

Pierre-Marie Pédrot (Apr 04 2017 at 00:09):

well, you could probably remove coq altogether

Pierre-Marie Pédrot (Apr 04 2017 at 00:09):

and use LEAN

Pierre-Marie Pédrot (Apr 04 2017 at 00:09):

that's C++

Pierre-Marie Pédrot (Apr 04 2017 at 00:09):

safest of the safest

Pierre-Marie Pédrot (Apr 04 2017 at 00:09):

look ma, no garbage collection

Maxime Dénès (Apr 04 2017 at 00:10):

they don't need to, they don't allocate arrays like crazy :D

Pierre-Marie Pédrot (Apr 04 2017 at 00:10):

I'm waiting for the implementation of Coqonut

Pierre-Marie Pédrot (Apr 04 2017 at 00:10):

Tomorrow by 2pm, is that possible?

Pierre-Marie Pédrot (Apr 04 2017 at 00:10):

OP delivered EConstr

Pierre-Marie Pédrot (Apr 04 2017 at 00:11):

Tomorrow is the day of insensitivity

Maxime Dénès (Apr 04 2017 at 00:11):

if I didn't have to fix all this mess, Coqonut would be already shipped :)

Maxime Dénès (Apr 04 2017 at 00:11):

do we have some mathcomp results?

Pierre-Marie Pédrot (Apr 04 2017 at 00:12):

Seems to be a failure

Maxime Dénès (Apr 04 2017 at 00:12):

oh but of course

Maxime Dénès (Apr 04 2017 at 00:13):

we didn't port it to EInstance

Maxime Dénès (Apr 04 2017 at 00:13):

I mean you didn't do it!

Pierre-Marie Pédrot (Apr 04 2017 at 00:13):

Too busy finding bugs in universes

Pierre-Marie Pédrot (Apr 04 2017 at 00:13):

and rewriting the kernel

Pierre-Marie Pédrot (Apr 04 2017 at 00:13):

and universe unification

Pierre-Marie Pédrot (Apr 04 2017 at 00:13):

and nsatz

Maxime Dénès (Apr 04 2017 at 00:14):

Ok, so let's do that tomorrow.

Pierre-Marie Pédrot (Apr 04 2017 at 00:14):

fine

Pierre-Marie Pédrot (Apr 04 2017 at 00:14):

I think I'll go to bed

Maxime Dénès (Apr 04 2017 at 00:14):

Meanwhile, enjoy the night, and thanks for your help!

Pierre-Marie Pédrot (Apr 04 2017 at 00:14):

you're welcome

Pierre-Marie Pédrot (Apr 04 2017 at 00:14):

I'm always interested in finding soundness issues

Pierre-Marie Pédrot (Apr 04 2017 at 00:14):

did you know we got cited in SIGBOVIK last year for that?

Maxime Dénès (Apr 04 2017 at 00:15):

lol really?

Pierre-Marie Pédrot (Apr 04 2017 at 00:15):

yep

Pierre-Marie Pédrot (Apr 04 2017 at 00:15):

http://sigbovik.org/2016/proceedings.pdf

Pierre-Marie Pédrot (Apr 04 2017 at 00:17):

UNPRL: NUPRL PROOF RE-EVALUATION LOGIC

Maxime Dénès (Apr 04 2017 at 00:17):

yeah I read

Maxime Dénès (Apr 04 2017 at 00:18):

not sure it is the best way to become famous :)

Pierre-Marie Pédrot (Apr 04 2017 at 00:18):

That's international fame come on

Pierre-Marie Pédrot (Apr 04 2017 at 00:18):

probably my best citation up to no

Pierre-Marie Pédrot (Apr 04 2017 at 00:18):

The ultimate SIGBOVIK 1 H-index

Pierre-Marie Pédrot (Apr 04 2017 at 00:19):

I should probably get some sleep

Maxime Dénès (Apr 04 2017 at 00:19):

yeah the only other could be a medal of honor for heroic battles on the Coq field

Pierre-Marie Pédrot (Apr 04 2017 at 00:19):

and some cheese

Pierre-Marie Pédrot (Apr 04 2017 at 00:19):

in an indistinct order

Pierre-Marie Pédrot (Apr 04 2017 at 00:19):

nobody cares

Pierre-Marie Pédrot (Apr 04 2017 at 00:19):

you can die for their freedom

Pierre-Marie Pédrot (Apr 04 2017 at 00:19):

this is AMERICA

Maxime Dénès (Apr 04 2017 at 00:19):

yep, see you tomorrow for more bugs and more fun

Pierre-Marie Pédrot (Apr 04 2017 at 00:19):

see you then

Emilio Jesús Gallego Arias (Apr 04 2017 at 01:35):

using opam to do benchmarking is like using NUPRL to make foie gras

Jason Gross (Apr 04 2017 at 03:11):

Hey, @Emilio Jesús Gallego Arias, if I point you at a branch or two in a development making heavy use of universes and rewriting in type, would you be {interested in,willing to} add it to the bench?

Pierre-Marie Pédrot (Apr 04 2017 at 10:07):

@Matej Košík @Enrico Tassi I'm not sure how to do, and you probably know better so I'm asking directly: could any of you write an OPAM package for the git VST ? I'd like to bench it on pendulum as well. Thanks.

Pierre-Marie Pédrot (Apr 04 2017 at 10:08):

https://github.com/PrincetonUniversity/VST

Pierre-Marie Pédrot (Apr 04 2017 at 10:08):

Theoretically HEAD compiles both with 8.6 and trunk.

Matej Košík (Gitter import) (Apr 04 2017 at 10:38):

@Pierre-Marie Pédrot Ok. I am on it.

Matej Košík (Gitter import) (Apr 04 2017 at 11:44):

@Pierre-Marie Pédrot I've created coq-vst package, added it to the set of benchmarked packages. It is safe to start benchmarking job. Right now I am trying to confirm that coq-vst can be installed with coq.8.6.dev and coq.dev. That will take some time.

Pierre-Marie Pédrot (Apr 04 2017 at 11:44):

@Matej Košík Thanks a lot!

Matej Košík (Gitter import) (Apr 04 2017 at 11:52):

@Pierre-Marie Pédrot You are welcome.

Maxime Dénès (Apr 04 2017 at 11:52):

@Pierre-Marie Pédrot I launched a new EConstr bench after merging your mathcomp PR.

Maxime Dénès (Apr 04 2017 at 11:52):

https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/34/console

Emilio Jesús Gallego Arias (Apr 04 2017 at 12:09):

@Jason Gross sure, let us know where the code is

Maxime Dénès (Apr 04 2017 at 13:35):

@Pierre-Marie Pédrot @Matthieu Sozeau have you seen the message of Beta on coqdev? Is it expected to have univ inconsistencies with -type-in-type?

Pierre-Marie Pédrot (Apr 04 2017 at 13:35):

I think it is, but I'm not a specialist of this code, @Matthieu Sozeau is probably better informed.

Matej Košík (Gitter import) (Apr 04 2017 at 14:52):

@Maxime Dénès The job you started has failed because there was a bug in the bencharmking script. I've fixed the bug, restarted the script but it will still fail because coq-mathcomp-ssreflect compilation (for the _old_ commit) fails to compile. For the _new_ commit all goes well.

Maxime Dénès (Apr 04 2017 at 14:53):

Yeah I'm working on it. We need to merge trunk into econstr.

Pierre-Marie Pédrot (Apr 04 2017 at 15:34):

Can I play with pendulum or should we bench EConstr first?

Matej Košík (Gitter import) (Apr 04 2017 at 15:36):

@Pierre-Marie Pédrot I am not doing anything there, right now...

Pierre-Marie Pédrot (Apr 04 2017 at 15:36):

@Maxime Dénès ?

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:00):

So any clue folks on where is the module system spending 1GiB to compile https://github.com/coq/coq/blob/trunk/theories/Structures/OrdersEx.v (see https://coq.inria.fr/bugs/show_bug.cgi?id=5270)

Pierre-Marie Pédrot (Apr 04 2017 at 16:02):

Well, that's not a huge amount of memory, is it?

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:03):

Just wondering, as it seems to be the file that uses most memory of the whole stdlib

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:03):

and it is relatively compact

Pierre-Marie Pédrot (Apr 04 2017 at 16:03):

Modules are known to be costly. Even the vo files are big.

Pierre-Marie Pédrot (Apr 04 2017 at 16:03):

Not mentionning the vio.

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:03):

yeah I see

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:03):

they have some non-linear growth factor it seems

Pierre-Marie Pédrot (Apr 04 2017 at 16:04):

You can use votour on the vio if you want to have an idea

Pierre-Marie Pédrot (Apr 04 2017 at 16:04):

yes, everything is duplicated when applying a module substittuion

Pierre-Marie Pédrot (Apr 04 2017 at 16:05):

AFAIR, the problem stems from the field Declarations.mod_type.

Pierre-Marie Pédrot (Apr 04 2017 at 16:05):

We ought to keep it abstract, but we expand it unconditionally, and bam.

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:10):

maybe it is the time to increase the density parameter of Coq

Pierre-Marie Pédrot (Apr 04 2017 at 16:11):

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:11):

to stop it expanding I mean

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:12):

I guess that making mod_type abstract is science fiction material, right?

Pierre-Marie Pédrot (Apr 04 2017 at 16:12):

That's worse, I'm not sure why it would make sense.

Pierre-Marie Pédrot (Apr 04 2017 at 16:13):

How making it abstract would sove the issue?

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:13):

Oh no clue myself, you had mentioned it

Pierre-Marie Pédrot (Apr 04 2017 at 16:13):

ah yeah, I misunderstood your statement

Pierre-Marie Pédrot (Apr 04 2017 at 16:14):

Abstract as in Coq, not as in OCaml

Pierre-Marie Pédrot (Apr 04 2017 at 16:14):

Well, I have no idea of the feasability

Pierre-Marie Pédrot (Apr 04 2017 at 16:14):

And the worst thing is that probably nobody has.

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:14):

I see, thanks

Pierre-Marie Pédrot (Apr 04 2017 at 16:14):

Because you know, modules.

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:15):

Yeah, modules are really opaque to me

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:15):

the way the obj system is organized, hard to dwell in

Pierre-Marie Pédrot (Apr 04 2017 at 16:15):

Obj system is not that bad.

Pierre-Marie Pédrot (Apr 04 2017 at 16:15):

You have to understand when the methods are called but that's about it.

Pierre-Marie Pédrot (Apr 04 2017 at 16:16):

Modules are really intricate, OTOH.

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:16):

libobject is quite incovenient to use in my scenarios, where I really want to inspect Coq's state live

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:16):

like let's say, from SerAPI

Pierre-Marie Pédrot (Apr 04 2017 at 16:17):

That's the wonder of existential types.

Pierre-Marie Pédrot (Apr 04 2017 at 16:17):

You could add a marshalling method if you like.

Pierre-Marie Pédrot (Apr 04 2017 at 16:18):

That's not very hard actually.

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:18):

all the subst_object stuff

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:18):

yeah it is not hard

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:18):

but incovenient

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:18):

I am not a fan of such "generic" stuff

Pierre-Marie Pédrot (Apr 04 2017 at 16:18):

Coq needs to be extensible, if you want to write e.g. plugins.

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:19):

extensible != generic stuff

Pierre-Marie Pédrot (Apr 04 2017 at 16:19):

What do you call generic?

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:19):

libobject

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:19):

contains very different objects

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:20):

with very different API

Pierre-Marie Pédrot (Apr 04 2017 at 16:20):

You don't like OOP?

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:20):

also the way classification works

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:20):

totally hinders following the data flow scheme

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:20):

it is a matter of responsibilites

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:20):

the module system should take of the disposal

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:20):

explicitly

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:20):

when closing modules etc

Pierre-Marie Pédrot (Apr 04 2017 at 16:20):

I agree that it would be better to have inversion of control

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:20):

instead this is delegated to the object, so you have no clue what is going on

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:20):

indeed

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:21):

you could of course, provide a proper extension API for the enviroment, etc...

Pierre-Marie Pédrot (Apr 04 2017 at 16:21):

If you start writing purely functional interface to libobject

Pierre-Marie Pédrot (Apr 04 2017 at 16:21):

that should become possible

Pierre-Marie Pédrot (Apr 04 2017 at 16:22):

I'm actually not sure this is that hard in the end.

Pierre-Marie Pédrot (Apr 04 2017 at 16:22):

We can always write imperative wrappers in the transition phase.

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:22):

yeah it was just a comment, but at least for me, the current control flow makes it one order of magnitude harder to understand the code path of closing a module

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:23):

it also makes it very hard to interact properly say, a new system of notations namespaces, with the current system

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:24):

but anyways it was just a comment

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:24):

how would such interface look like in your opinion PM?

Pierre-Marie Pédrot (Apr 04 2017 at 16:24):

I'd say that there is a blobby State.t

Pierre-Marie Pédrot (Apr 04 2017 at 16:24):

where you can add you own stuff.

Pierre-Marie Pédrot (Apr 04 2017 at 16:25):

and all the unit types of libobject are turned into some State.t -> State.t, maybe even returning a new object.

Pierre-Marie Pédrot (Apr 04 2017 at 16:25):

more precisely

Pierre-Marie Pédrot (Apr 04 2017 at 16:26):

a type quantified over the parts of the state that can be accessed by the function.

Pierre-Marie Pédrot (Apr 04 2017 at 16:26):

we can probably do that with GADTs.

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:26):

should that be merged with summary ?

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:26):

I'd say so

Pierre-Marie Pédrot (Apr 04 2017 at 16:26):

Well there would not be a real need of summary afterwards

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:27):

that's something worthwhile to pursue

Pierre-Marie Pédrot (Apr 04 2017 at 16:27):

yep

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:27):

the key question is what the structure of State.t should be

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:27):

indeed you have proof state, section state

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:27):

somehow you would like to expose the section org

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:30):

Something we have problems handling in the stm indeed is sectioning and modules

Pierre-Marie Pédrot (Apr 04 2017 at 16:30):

There are fishy things in the kernel about both sections and modules anyway

Pierre-Marie Pédrot (Apr 04 2017 at 16:36):

Is @Maxime Dénès around? I'd like to have a few PR merged.

Pierre-Marie Pédrot (Apr 04 2017 at 16:36):

That includes EConstr :bomb:

Emilio Jesús Gallego Arias (Apr 04 2017 at 16:42):

:shipit:

Maxime Dénès (Apr 04 2017 at 18:27):

@Pierre-Marie Pédrot I'm not far

Maxime Dénès (Apr 04 2017 at 18:27):

can you make the list?

Pierre-Marie Pédrot (Apr 04 2017 at 18:29):

#434 : no real complains from people, @Enrico Tassi lamenting we need to do the compiler job

Pierre-Marie Pédrot (Apr 04 2017 at 18:30):

#400 : @Matthieu Sozeau happy but not @silene

Pierre-Marie Pédrot (Apr 04 2017 at 18:30):

#508 : seemingly uncontroversial

Pierre-Marie Pédrot (Apr 04 2017 at 18:31):

#519 : @Enrico Tassi complaining, but off-topic I think

Pierre-Marie Pédrot (Apr 04 2017 at 18:31):

and then a few more which need more testing and discussion.

Pierre-Marie Pédrot (Apr 04 2017 at 18:34):

ah and obviously :

Pierre-Marie Pédrot (Apr 04 2017 at 18:34):

#379 : the one PR to rule them and and in insensitivity bind them

Emilio Jesús Gallego Arias (Apr 04 2017 at 19:10):

oh, related to Pierre-Marie PRs, I've got my flambda patch ready, will submit tomorrow; how should we integrate it into benchmarking? @Matej Košík , are configure options implemented?

Emilio Jesús Gallego Arias (Apr 04 2017 at 19:24):

Also, is there a possibility that #434 / #400 may affect adversely flambda ?

Pierre-Marie Pédrot (Apr 04 2017 at 19:24):

#434 is independent from Flambda AFAICT.

Pierre-Marie Pédrot (Apr 04 2017 at 19:26):

I don't think Flambda will affect adversely #400. At worst it would subsume the patch.

Pierre-Marie Pédrot (Apr 04 2017 at 19:26):

Thankfully we can bench!

Emilio Jesús Gallego Arias (Apr 04 2017 at 19:26):

well yeah maybe we should test

Emilio Jesús Gallego Arias (Apr 04 2017 at 19:26):

in this cases I'd love to have CPP{,O} support in Ocaml/Coq

Emilio Jesús Gallego Arias (Apr 04 2017 at 19:27):

so we could define #OPTIM

Emilio Jesús Gallego Arias (Apr 04 2017 at 19:27):

at least for development releases, so your patch could be merged, and I could still pass something like -D DISABLE_OPTIM to Coq to test how well flambda is going

Pierre-Marie Pédrot (Apr 04 2017 at 19:28):

We can do that with a PPX

Pierre-Marie Pédrot (Apr 04 2017 at 19:29):

and by the miracle of OCaml 4.02 we do have ppx around

Emilio Jesús Gallego Arias (Apr 04 2017 at 19:32):

ppx seems a bit overkill, I wish we didn't have to roll our own system, but to reuse cpp cppo

Emilio Jesús Gallego Arias (Apr 04 2017 at 19:32):

on the other hand, by Pierre-Marie's law, if it can be abused, it will be abused

Emilio Jesús Gallego Arias (Apr 04 2017 at 19:32):

so I fear adding #ifdefs to Coq

Matej Košík (Gitter import) (Apr 04 2017 at 19:54):

@Emilio Jesús Gallego Arias No.

Pierre-Marie Pédrot (Apr 04 2017 at 22:01):

@Matej Košík I don't get why the compilation of math-comp on pendulum fails : https://ci.inria.fr/coq/job/benchmark-part-of-the-branch/41/consoleFull.

Pierre-Marie Pédrot (Apr 04 2017 at 22:01):

It seems it uses a branch that has been ported to EConstr, but I don't know who decides that in the first place.

Maxime Dénès (Apr 04 2017 at 23:07):

@Pierre-Marie Pédrot hum, what is happening again?

Pierre-Marie Pédrot (Apr 04 2017 at 23:07):

Where?

Maxime Dénès (Apr 04 2017 at 23:08):

on pendulum

Pierre-Marie Pédrot (Apr 04 2017 at 23:08):

Ah! I don't know.

Pierre-Marie Pédrot (Apr 04 2017 at 23:09):

This machine seems a bit capricious if you ask me

Maxime Dénès (Apr 04 2017 at 23:13):

The one I launched before leaving was: https://ci.inria.fr/coq/job/benchmark-part-of-the-branch/37/console

Maxime Dénès (Apr 04 2017 at 23:13):

I don't understand why it failed

Pierre-Marie Pédrot (Apr 04 2017 at 23:14):

That one failed because math-comp was not ported to the change of GLetIn in master it seems

Pierre-Marie Pédrot (Apr 04 2017 at 23:16):

Wait this did not get merged yet?

Maxime Dénès (Apr 04 2017 at 23:16):

I thought I had merged it precisely before launching this build.

Maxime Dénès (Apr 04 2017 at 23:17):

Let me try with a more specific commit sha1.

Maxime Dénès (Apr 04 2017 at 23:17):

Oh but I see!!

Maxime Dénès (Apr 04 2017 at 23:17):

I didn't merge ssr's fix to my econstr branch. I'm stupid.

Pierre-Marie Pédrot (Apr 04 2017 at 23:18):

Still, in my case it is picking the math-comp:econstr branch, and this is not the right one.

Pierre-Marie Pédrot (Apr 04 2017 at 23:19):

I want math-comp:master, and didn't ask for anything

Maxime Dénès (Apr 04 2017 at 23:22):

Yeah the script has been hijacked for that.

Pierre-Marie Pédrot (Apr 04 2017 at 23:22):

Grrr

Maxime Dénès (Apr 04 2017 at 23:22):

Because overlays are being implemented by @Matej Košík.

Maxime Dénès (Apr 04 2017 at 23:22):

Did you see #539?

Pierre-Marie Pédrot (Apr 04 2017 at 23:23):

Like I have time to read other's PR

Pierre-Marie Pédrot (Apr 04 2017 at 23:23):

I'm writing them sir

Pierre-Marie Pédrot (Apr 04 2017 at 23:24):

Oh, that's just like 6 minutes ago

Pierre-Marie Pédrot (Apr 04 2017 at 23:24):

I was wondering why I hadn't seen it

Maxime Dénès (Apr 04 2017 at 23:25):

Yeah, sorry, it's unrelated and I wasn't expecting you to have read it already.

Maxime Dénès (Apr 04 2017 at 23:25):

But we surely need to merge EConstr before this :)

Pierre-Marie Pédrot (Apr 04 2017 at 23:25):

I'm hoping for the removal of unification though

Maxime Dénès (Apr 04 2017 at 23:26):

removal of unification = removal of apply

Pierre-Marie Pédrot (Apr 04 2017 at 23:27):

yeah, nice equation

Pierre-Marie Pédrot (Apr 04 2017 at 23:27):

I'm in, where do I have to sign?

Maxime Dénès (Apr 04 2017 at 23:27):

so removal of unification means new tactics

Maxime Dénès (Apr 04 2017 at 23:27):

at least for apply

Maxime Dénès (Apr 04 2017 at 23:28):

now the question is, why reimplement one that is different from ssr's apply?

Pierre-Marie Pédrot (Apr 04 2017 at 23:28):

I don't care, just want unification.ml gone

Pierre-Marie Pédrot (Apr 04 2017 at 23:29):

do you happen to know how to time HoTT?

Pierre-Marie Pédrot (Apr 04 2017 at 23:29):

I'm using the timing-html target, but I get a too detailed result

Maxime Dénès (Apr 04 2017 at 23:29):

I think you care but you don't know: shouldn't we take the easiest path toward removal of unification.ml?

Maxime Dénès (Apr 04 2017 at 23:29):

sorry, I don't know

Pierre-Marie Pédrot (Apr 04 2017 at 23:29):

Any path is good

Pierre-Marie Pédrot (Apr 04 2017 at 23:30):

What about my PRs?

Pierre-Marie Pédrot (Apr 04 2017 at 23:30):

I'm going to harass you until I get a least the two less uncontroversial merged

Pierre-Marie Pédrot (Apr 04 2017 at 23:30):

(this does not include EConstr)

Maxime Dénès (Apr 04 2017 at 23:30):

ok, here is one thing I need to understand

Maxime Dénès (Apr 04 2017 at 23:30):

is there a chance that they are subsumed by flambda?

Pierre-Marie Pédrot (Apr 04 2017 at 23:31):

I'd say only #400 potentially

Pierre-Marie Pédrot (Apr 04 2017 at 23:31):

the array mapping is untouched by Flambda AFAICT

Pierre-Marie Pédrot (Apr 04 2017 at 23:32):

and the others are not micro optimizations

Pierre-Marie Pédrot (Apr 04 2017 at 23:32):

they're real algorithmic reworking

Maxime Dénès (Apr 04 2017 at 23:32):

ok, let me review briefly and merge #434 now

Pierre-Marie Pédrot (Apr 04 2017 at 23:33):

A few of the PR can be considered as bugfixes for 8.6

Maxime Dénès (Apr 04 2017 at 23:34):

ah ah!

Maxime Dénès (Apr 04 2017 at 23:34):

which one for instance?

Pierre-Marie Pédrot (Apr 04 2017 at 23:35):

#537

Pierre-Marie Pédrot (Apr 04 2017 at 23:35):

A part of #532

Pierre-Marie Pédrot (Apr 04 2017 at 23:35):

(which I can extract)

Maxime Dénès (Apr 04 2017 at 23:35):

Oh, I missed that one because it was not in your list.

Pierre-Marie Pédrot (Apr 04 2017 at 23:36):

#519

Maxime Dénès (Apr 04 2017 at 23:36):

Ok, I'll merge #434 in trunk first.

Pierre-Marie Pédrot (Apr 04 2017 at 23:36):

Probably not all of #519 because it changes the representation of summary

Pierre-Marie Pédrot (Apr 04 2017 at 23:37):

yay!

Maxime Dénès (Apr 04 2017 at 23:39):

For #519, @Enrico Tassi still hasn't cleared his request for changes, I'll ping him tomorrow.

Pierre-Marie Pédrot (Apr 04 2017 at 23:42):

BTW, we can make a political coup if you're afraid of HoTT slowness in EConstr

Maxime Dénès (Apr 04 2017 at 23:42):

WDYM concretely?

Pierre-Marie Pédrot (Apr 04 2017 at 23:42):

There is a huge portion of the time spent in hashconsing of universes

Pierre-Marie Pédrot (Apr 04 2017 at 23:42):

We can deactivate it

Maxime Dénès (Apr 04 2017 at 23:42):

lol

Pierre-Marie Pédrot (Apr 04 2017 at 23:42):

and trick them into believing EConstr is faster

Maxime Dénès (Apr 04 2017 at 23:43):

I'd rather see a fully independent bench with hashconsing of universes disabled to see if it is faster

Pierre-Marie Pédrot (Apr 04 2017 at 23:43):

@Jason Gross you didn't hear anything

Pierre-Marie Pédrot (Apr 04 2017 at 23:43):

That's a one-line change

Pierre-Marie Pédrot (Apr 04 2017 at 23:43):

I can submit a PR

Maxime Dénès (Apr 04 2017 at 23:44):

speaking of benches, this one seems to be going through: https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/43/console

Maxime Dénès (Apr 04 2017 at 23:44):

So I'll leave it here for today and finish reviewing your optim PRs tomorrow, pinging people when necessary

Pierre-Marie Pédrot (Apr 04 2017 at 23:45):

Fine with me.

Matej Košík (Gitter import) (Apr 05 2017 at 05:21):

@Maxime Dénès @Pierre-Marie Pédrot Nothing runs on pendulum now so I am going to take advantage of that and test overlays.

Maxime Dénès (Apr 05 2017 at 05:56):

@Matej Košík sounds good!

Matej Košík (Gitter import) (Apr 05 2017 at 06:38):

Ok. Overlays work. coq-vst benchmarking is being tested (but seems to work). Today I'll try to fix this.

Matej Košík (Gitter import) (Apr 05 2017 at 06:42):

@Maxime Dénès On pendulum, I've copied the original coq-bench (with your modified OPAM archive with your custom stuff) to coq-bench.bak. You'll find it there.

Maxime Dénès (Apr 05 2017 at 08:19):

@Matej Košík ok, thanks!

Emilio Jesús Gallego Arias (Apr 05 2017 at 10:45):

So indeed, what is the plan to integrate coq-bench and travis, @Maxime Dénès @Matej Košík ?

Maxime Dénès (Apr 05 2017 at 10:51):

@Pierre-Marie Pédrot I'm launching a line-by-line bench of integral_char

Maxime Dénès (Apr 05 2017 at 10:51):

@Emilio Jesús Gallego Arias Maybe the best is to discuss it next week when you are here?

Emilio Jesús Gallego Arias (Apr 05 2017 at 12:04):

Oh sure, I'd be great to converge

Pierre-Marie Pédrot (Apr 05 2017 at 12:05):

@Maxime Dénès I've commented the EConstr PR, but I think I found a major source of slowness.

Pierre-Marie Pédrot (Apr 05 2017 at 12:29):

@Maxime Dénès Could you launch a pendulum bench with the patch I just pushed?

Maxime Dénès (Apr 05 2017 at 12:29):

Sure!

Emilio Jesús Gallego Arias (Apr 05 2017 at 12:36):

Hey folks, how would a patch providing an option to disable VM reduction (in proofs/redexp.ml be received?

Pierre-Marie Pédrot (Apr 05 2017 at 12:37):

Isn't there already such a thing? It rings a bell.

Emilio Jesús Gallego Arias (Apr 05 2017 at 12:37):

only for native compute

Emilio Jesús Gallego Arias (Apr 05 2017 at 12:37):

AFAICT

Emilio Jesús Gallego Arias (Apr 05 2017 at 12:38):

my motivation is that in jscoq I have to disable it manually, otherwise many users can't use ring, etc... however I would really like it to be a flag as losing vm_compute is a pain when compiling the contribs that jscoq ships

Pierre-Marie Pédrot (Apr 05 2017 at 12:40):

Well, that looks useful.

Emilio Jesús Gallego Arias (Apr 05 2017 at 12:41):

yeah my original plan was to port