Stream: Coq devs & plugin devs

Topic: imported from gitter room coq/coq


view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:43):

Hooooooola colegas! coq/coq#523 has already produced some discussion

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:43):

it is cool how the link system works thou

view this post on Zulip Théo Zimmermann (Mar 28 2017 at 14:54):

It is cool as changes to Markdown files can be previewed as rendered Markdown in GitHub ^^

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:54):

Salut Theo !

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:54):

I have always resisting using this stuff myself

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:54):

but yeah

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:54):

I guess I am hipster now

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:54):

:D

view this post on Zulip Théo Zimmermann (Mar 28 2017 at 14:54):

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/

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:54):

indeed it could be useful for the reasons we mentioned

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:55):

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

view this post on Zulip Théo Zimmermann (Mar 28 2017 at 14:56):

Well Gitter certainly has this advantage over the others ^^

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:56):

ok cool so let's stick to it for now

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:56):

yeah in fact I think Maxime mentioned that

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:57):

short on time these days xD

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

these days all happens like

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

one to one

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

and it is very redudant

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

if Travis break

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

etc..

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

and we where abusing the comment section of github a bit

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

doing PRCHAT

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

so this may help

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:58):

it may not XD

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 14:59):

the PR was my own thing XD

view this post on Zulip Théo Zimmermann (Mar 28 2017 at 14:59):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:00):

ok let's see how this works

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:00):

I am not a user myself of IRC

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:00):

since 1997

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:00):

or so

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:00):

yeah I found it hard to follow

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:01):

yeah so lets try to keep the chat efficient

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:01):

I guess people is not really supposed to follow this

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:01):

in the sense

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:01):

that relevant issues

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:01):

will be always get a bug or a PR

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:02):

but indeed a few things can be helpful

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:02):

questions

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:02):

this kinda overlaps with coqdev

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:02):

I dunno

view this post on Zulip Théo Zimmermann (Mar 28 2017 at 15:02):

yes it does

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:02):

this is why I always refused to use gitter

view this post on Zulip Théo Zimmermann (Mar 28 2017 at 15:02):

as much as SO overlaps with coq-club

view this post on Zulip Théo Zimmermann (Mar 28 2017 at 15:02):

but still I prefer SO to coq-club

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:02):

but lets be open

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:02):

yeah I know what you man

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:02):

mean

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:03):

subtle details in the interface

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:03):

do make a big difference

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:03):

hihi

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:03):

this is maybe a good forum

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:03):

to discuss about which PR

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:03):

should be fast-tracked

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:04):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:05):

dedicated to the release manager

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:05):

sure sorry about that!

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:05):

I'll stop the useless chat

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

^^

view this post on Zulip Théo Zimmermann (Mar 28 2017 at 15:08):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:09):

I had to click in "more coq rooms"

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:09):

and join

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

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

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

+1

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:18):

It looks cool

view this post on Zulip Théo Zimmermann (Mar 28 2017 at 15:18):

:smile:

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

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

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

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:25):

let me have a fresh look to it

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

view this post on Zulip Théo Zimmermann (Mar 28 2017 at 15:28):

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:29):

So the initial idea looks good IMO

view this post on Zulip Théo Zimmermann (Mar 28 2017 at 15:30):

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:31):

I am not an admin on that repository

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

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

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

view this post on Zulip Théo Zimmermann (Mar 28 2017 at 15:35):

Ah OK

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:35):

the coq-ceps I mean

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:50):

I am gonna test the GH integration

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 15:50):

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

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

view this post on Zulip Maxime Dénès (Mar 28 2017 at 16:13):

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

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

view this post on Zulip Maxime Dénès (Mar 28 2017 at 16:13):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 16:14):

it requires adding a hook to the coq repos

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 16:14):

that is

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

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

view this post on Zulip Maxime Dénès (Mar 28 2017 at 18:02):

does the write access need to stay?

view this post on Zulip Maxime Dénès (Mar 28 2017 at 18:02):

or is it just for setting it up?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 18:04):

it is just for setting up I guess

view this post on Zulip Maxime Dénès (Mar 28 2017 at 18:09):

it should be ok

view this post on Zulip Maxime Dénès (Mar 28 2017 at 18:09):

no need to give write access in fact

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 18:10):

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

view this post on Zulip Maxime Dénès (Mar 28 2017 at 18:10):

btw there is a Travis integration as well

view this post on Zulip Maxime Dénès (Mar 28 2017 at 18:10):

I could set that up

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 18:11):

P:Prop,P\forall P : Prop , P

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 18:11):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 18:11):

I personally have no opinion on the room structure

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 18:11):

I think the travis room makes sense

view this post on Zulip Maxime Dénès (Mar 28 2017 at 18:12):

coq/travis?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2017 at 18:12):

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

view this post on Zulip Théo Zimmermann (Mar 28 2017 at 19:38):

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

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

view this post on Zulip Maxime Dénès (Mar 29 2017 at 08:17):

what would you use instead?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 08:19):

even debbugs would be better XD

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 08:21):

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

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

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

view this post on Zulip Maxime Dénès (Mar 29 2017 at 11:55):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 11:55):

you gotta be careful with application

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 11:55):

that was a highly controversial at OPLSS 2013

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 11:56):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 11:56):

how many things would break?

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

view this post on Zulip Maxime Dénès (Mar 29 2017 at 12:03):

you don't want to know :smile:

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 12:07):

the set of constraints was ordered differently

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 12:07):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 12:07):

what is the bug doing to unification.ml?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 12:08):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 12:09):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 12:09):

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:17):

+1

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

view this post on Zulip Théo Zimmermann (Mar 29 2017 at 13:18):

But I can answer you here.

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:19):

Oh please

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:19):

answer here

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:22):

maybe we should just poll support for Bugzilla first

view this post on Zulip Théo Zimmermann (Mar 29 2017 at 13:22):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:22):

and then try to build another replacement

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:22):

but oh man

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:22):

this is not Coq

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:22):

it is more like a Turtle

view this post on Zulip Théo Zimmermann (Mar 29 2017 at 13:23):

^^

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:23):

I can't understand why.
political reasons

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:23):

I can understand why

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:23):

where to host the code has IMO important political significance

view this post on Zulip Théo Zimmermann (Mar 29 2017 at 13:23):

Yeah but political reasons are used in a inconsistent fashion

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:23):

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

view this post on Zulip Théo Zimmermann (Mar 29 2017 at 13:23):

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

view this post on Zulip Théo Zimmermann (Mar 29 2017 at 13:24):

it is, yes

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:24):

XD

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:24):

anyways

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:24):

so what about the CEP?

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:26):

well it is tightly couple AFAICT

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:26):

in the same way ring and reals are

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:27):

I would rather say

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:27):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:27):

many things were outside

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:27):

like Program / Obligation

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:27):

and now are "inside"

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:27):

so imagine the case for Program

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:27):

if includes were of the from

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:28):

From Program Require XX

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:28):

Why to change it when it was merged?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:28):

I like namespaces, so this is a very personal opinion

view this post on Zulip Théo Zimmermann (Mar 29 2017 at 13:28):

Well now it is From Coq Require Program.XX

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

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

view this post on Zulip Théo Zimmermann (Mar 29 2017 at 13:29):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:29):

every time the user types "From XXX Require UU"

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:29):

it will donwload it

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:29):

and all the packages will live in the same namespace

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:30):

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

view this post on Zulip Théo Zimmermann (Mar 29 2017 at 13:30):

oh I fully agree with you on that point

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:31):

there are things that are officially supported

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:31):

either by the Coq Developers

view this post on Zulip Théo Zimmermann (Mar 29 2017 at 13:31):

Well, you were not the one proposing it anyways

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:31):

or by other persons

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:31):

I just don't care

view this post on Zulip Théo Zimmermann (Mar 29 2017 at 13:31):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:32):

in opam I usually don't care about the provenance

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:32):

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

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:35):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:36):

And IMHO you need them

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 13:44):

they won't be compatible

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 15:51):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 15:51):

@Maxime Dénès sure I think so

view this post on Zulip Maxime Dénès (Mar 29 2017 at 15:51):

oups sorry

view this post on Zulip Maxime Dénès (Mar 29 2017 at 15:51):

wrong channel

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 15:52):

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

view this post on Zulip Maxime Dénès (Mar 29 2017 at 15:52):

sure

view this post on Zulip Maxime Dénès (Mar 29 2017 at 15:53):

I'll do a pass of merges later tonight

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 15:53):

great

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 15:53):

I have little on the queue

view this post on Zulip Maxime Dénès (Mar 29 2017 at 15:53):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 15:53):

that's great

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 15:53):

I saw your latest push

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 15:54):

so that should be OK

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 15:54):

#441 will likely introduce some minor annoyances

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 15:55):

maybe the toplevel shows goals in differente cases

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 15:55):

but all of that should be minor

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 15:55):

again it is hard to test interactive behavior

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 15:55):

wrt to CoqIDE however

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 15:56):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 15:56):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 15:56):

the main difference is that now

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 15:56):

at every size change, coqide will repaint the goal window

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 15:56):

previously, it only repainted when sending a command

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 15:59):

vscode is free software and runs reasonably well

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 16:01):

also #502 should be IMHO merged

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 16:03):

So that is my queue:

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 16:05):

that's all

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 16:08):

seems exaclty like that

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

view this post on Zulip Théo Zimmermann (Mar 29 2017 at 17:20):

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

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

view this post on Zulip Théo Zimmermann (Mar 29 2017 at 17:22):

well maybe 24 days ago is not so recent

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 17:30):

so indeed

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

view this post on Zulip Théo Zimmermann (Mar 29 2017 at 17:32):

oh really that deadline passed? :(

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

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 21:55):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 21:55):

so at least we are good here

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 21:56):

this is IMO nice as all the clients build modularly now

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 21:56):

both the jscoq and serapi toplevel build this way

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 21:58):

I do think that splitting CoqIDE has many benefits

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 21:58):

yeah that is not worth it

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 21:59):

but about CoqIDE

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 21:59):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 21:59):

anyways, about CoqIDe

view this post on Zulip Maxime Dénès (Mar 29 2017 at 21:59):

does it build the VM?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 21:59):

it would greatly benefit from independent releases

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 21:59):

and of having easy branching

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 21:59):

branches

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 22:00):

well, that is for building against a normally built Coq

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 22:00):

but my ocamlbuild tree indeed does build the VM

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 22:00):

let me see the status of that

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 22:01):

but it does work

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 22:01):

just needs polishing, no special difficulty

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 22:02):

as you can use it to build the upper layers

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 22:02):

coqide, etc..

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 22:02):

which don't really benefit from paralellism

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 22:02):

and build the lower layers the usual way

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 22:02):

the cma in the META files

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 22:03):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 22:03):

that is to say

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 22:03):

the summary of that discussion is

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 22:05):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2017 at 22:05):

and then we follow suit

view this post on Zulip Maxime Dénès (Mar 29 2017 at 22:06):

ok thanks !

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

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

view this post on Zulip Maxime Dénès (Mar 30 2017 at 07:49):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 08:12):

cool thanks

view this post on Zulip Maxime Dénès (Mar 30 2017 at 09:09):

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

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 12:48):

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

view this post on Zulip Maxime Dénès (Mar 30 2017 at 13:30):

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

view this post on Zulip Maxime Dénès (Mar 30 2017 at 13:30):

I thought you'd do it :)

view this post on Zulip Théo Zimmermann (Mar 30 2017 at 13:47):

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

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

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

view this post on Zulip Théo Zimmermann (Mar 30 2017 at 13:48):

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 13:51):

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

view this post on Zulip Théo Zimmermann (Mar 30 2017 at 13:51):

Well there is an edit function

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 13:51):

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

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 13:52):

I mean, right now.

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 13:52):

We ougtha admit it, our dream has become true!

view this post on Zulip Théo Zimmermann (Mar 30 2017 at 13:52):

:D

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 13:54):

EConstr is almost ready to go, right?

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 13:54):

I hope so...

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 13:55):

fantastic

view this post on Zulip Théo Zimmermann (Mar 30 2017 at 13:56):

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 13:56):

Uhhh

view this post on Zulip Maxime Dénès (Mar 30 2017 at 13:56):

@Pierre-Marie Pédrot No :)

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 13:57):

anything ending in "z" cannot be any good

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

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

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 13:58):

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 14:00):

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

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

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

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

view this post on Zulip Maxime Dénès (Mar 30 2017 at 14:01):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 14:01):

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

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 14:01):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 14:02):

arguments are overrated

view this post on Zulip Maxime Dénès (Mar 30 2017 at 14:02):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 14:02):

the STM manages to do everything without them

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

view this post on Zulip Maxime Dénès (Mar 30 2017 at 14:02):

A very common paradigm in baroque programming.

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 14:03):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 14:04):

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

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

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 14:04):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 14:05):

That is just for convenience when doing CPS

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 14:05):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 14:05):

we must retain some elegance

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 14:05):

purely imperative CPS

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 14:05):

No more slacking around on this chat!

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 14:05):

ok

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 14:05):

yeah

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 14:05):

right!

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

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 14:06):

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 14:07):

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

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

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

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

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

view this post on Zulip Théo Zimmermann (Mar 30 2017 at 14:12):

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

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

view this post on Zulip Théo Zimmermann (Mar 30 2017 at 14:14):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 14:17):

Great!

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

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

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

view this post on Zulip Maxime Dénès (Mar 30 2017 at 14:24):

Ah ah! Well done :)

view this post on Zulip Maxime Dénès (Mar 30 2017 at 14:24):

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 14:30):

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

view this post on Zulip Maxime Dénès (Mar 30 2017 at 14:31):

I'll let @matejkosik give more details :)

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 14:32):

okk

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

view this post on Zulip Maxime Dénès (Mar 30 2017 at 14:42):

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

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 14:42):

Nope.

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 14:43):

I've rebased against yours before commiting.

view this post on Zulip Maxime Dénès (Mar 30 2017 at 14:43):

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

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 14:43):

Probably.

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

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

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 14:44):

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

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

view this post on Zulip Maxime Dénès (Mar 30 2017 at 14:45):

Not long, it reached CompCert already

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 14:45):

How many times are you benching each package?

view this post on Zulip Maxime Dénès (Mar 30 2017 at 14:45):

once only

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

view this post on Zulip Maxime Dénès (Mar 30 2017 at 14:46):

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

view this post on Zulip Maxime Dénès (Mar 30 2017 at 14:46):

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

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 14:46):

-_-

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

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

view this post on Zulip Maxime Dénès (Mar 30 2017 at 14:48):

So it should be faster now.

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

view this post on Zulip Maxime Dénès (Mar 30 2017 at 14:52):

Mathcomp is split in many packages...

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 15:06):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 15:06):

XD

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 15:07):

it is beautiful, amazing

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 15:09):

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

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

view this post on Zulip Maxime Dénès (Mar 30 2017 at 15:11):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 15:13):

to @jenkins folks

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 15:13):

whoever they are

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 15:45):

well @silene has a point with the comment

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 15:45):

maybe you should just folks use flambda

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 15:45):

and let non flambda users pay the cost

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 15:46):

Flambda cannot make wonders I'm afraid.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 15:46):

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

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

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

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:34):

Why not on the main coq page?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:34):

I think we could just have the wiki there

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

view this post on Zulip Théo Zimmermann (Mar 30 2017 at 17:34):

Two reasons:

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:35):

¡Hola @Jason Gross !

view this post on Zulip Théo Zimmermann (Mar 30 2017 at 17:35):

1) this is specifically linked to CEPs

view this post on Zulip Jason Gross (Mar 30 2017 at 17:35):

Hi!

view this post on Zulip Théo Zimmermann (Mar 30 2017 at 17:35):

Hi

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

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

view this post on Zulip Théo Zimmermann (Mar 30 2017 at 17:36):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:38):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:38):

I can't see where the CEP process is going

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

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

Well, I like the CEP process a lot.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:38):

So far what are the results?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:38):

How many CEPs turned into something real?

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

I think it helps take decisions which were really thought through

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:39):

such as?

view this post on Zulip Théo Zimmermann (Mar 30 2017 at 17:39):

Several, let me count

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:39):

do you have an example

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

view this post on Zulip Théo Zimmermann (Mar 30 2017 at 17:41):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:42):

associated at each CEP

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:42):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:42):

etc...

view this post on Zulip Théo Zimmermann (Mar 30 2017 at 17:43):

How so?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:43):

Same repository

view this post on Zulip Théo Zimmermann (Mar 30 2017 at 17:43):

And?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:43):

vs ceps-wiki / coq-wiki

view this post on Zulip Théo Zimmermann (Mar 30 2017 at 17:43):

But doc is not in a wiki anyways

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:43):

Oh some of it is

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:43):

in Cocoriko

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:43):

that hopefully is migrated to coq / coq

view this post on Zulip Théo Zimmermann (Mar 30 2017 at 17:44):

Yes, well it's mostly outdated doc

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:44):

anyways a good proof of the overhead

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:44):

is that actually we cannot get CEP merged

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:44):

or touch anything in the coq-ceps

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:44):

because some permission problem

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:44):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:44):

IMHO

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:44):

if we have a wiki

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:44):

we should have a single one

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:44):

for Coq

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:45):

that means

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:45):

cocorico is out if we add another wiki

view this post on Zulip Théo Zimmermann (Mar 30 2017 at 17:45):

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

view this post on Zulip Théo Zimmermann (Mar 30 2017 at 17:45):

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:46):

@Maxime Dénès

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 17:46):

I mean

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 18:00):

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

view this post on Zulip Maxime Dénès (Mar 30 2017 at 18:01):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 18:02):

Githubs wikis are just git repositories with markdown.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 30 2017 at 18:02):

so that is not _too_ bad

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

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 18:03):

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

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

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

view this post on Zulip Maxime Dénès (Mar 30 2017 at 18:04):

But jenkins doesn't use overlays AFAIK

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 18:04):

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

view this post on Zulip Maxime Dénès (Mar 30 2017 at 18:05):

What fix does CompCert need for EConstr ?!

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 18:05):

I mean mathcomp, sorry.

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

view this post on Zulip Maxime Dénès (Mar 30 2017 at 18:06):

I'll investigate

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

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

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

view this post on Zulip Maxime Dénès (Mar 30 2017 at 18:50):

oh fuck I know why

view this post on Zulip Maxime Dénès (Mar 30 2017 at 18:50):

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

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

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

view this post on Zulip Pierre-Marie Pédrot (Mar 30 2017 at 19:07):

There you go...

view this post on Zulip Maxime Dénès (Mar 30 2017 at 19:33):

@Pierre-Marie Pédrot Ok, this time the bench really started.

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 09:07):

In particular for hott, right?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 09:07):

Was it make timing

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 09:07):

@Jason Gross ?

view this post on Zulip Maxime Dénès (Mar 31 2017 at 09:35):

Yeah we need something more detailed.

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 11:09):

It is WIP as it needs some tweaks, namely:

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 12:44):

¡Hola @Matej Košík! Comment vas tu ?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 12:44):

I didn't know romance languages were allowed here.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 12:47):

I love romance

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:28):

@Pierre-Marie Pédrot whas is universe normalization? Is it the same as minimization?

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:28):

what is*

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

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

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:33):

ah! Like a local universe can become a global one?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:33):

Yep.

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:34):

Universe-operating functions ought to be insensitive as well (cough cough).

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:34):

Oh my god.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:34):

Indeed.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:35):

Luckily, the attack surface is way smaller than with evars.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:35):

Although one should be afraid of Type u being unified to Set / Prop.

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

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:36):

Can I spam pendulum with benchmarks btw?

view this post on Zulip Matej Košík (Gitter import) (Mar 31 2017 at 14:36):

Ok.

view this post on Zulip Matej Košík (Gitter import) (Mar 31 2017 at 14:36):

Well, I am not sure what is the protocol?\

view this post on Zulip Matej Košík (Gitter import) (Mar 31 2017 at 14:36):

Do we want to run the benchmarks always via Jenkins?

view this post on Zulip Matej Košík (Gitter import) (Mar 31 2017 at 14:37):

Is hat sufficient?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:37):

I don't know, I'm happy with the ci interface.

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

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

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:38):

But I think what PMP is really asking is if your script has stabilized

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:38):

Yes, I meant that.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 14:39):

@Matej Košík je suis emmerdé avec l'ANR

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

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:40):

Have you pulled the latest version?

view this post on Zulip Matej Košík (Gitter import) (Mar 31 2017 at 14:40):

The script should behave consistently with the open/closed status of the issues.

view this post on Zulip Matej Košík (Gitter import) (Mar 31 2017 at 14:41):

(on github)

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:41):

For other people, you mean here: https://github.com/coq/coq-bench/issues

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:41):

Universe rocket launched on pendulum. Let's see what happens.

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

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

view this post on Zulip Matej Košík (Gitter import) (Mar 31 2017 at 14:42):

@Pierre-Marie Pédrot +1

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:43):

@Emilio Jesús Gallego Arias Well, what do you propose?

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 14:43):

@Pierre-Marie Pédrot "dereference fault"?

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:43):

"existential delirium"?

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 14:44):

"functions not properly dereferencing evars?

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:45):

I like existential delirium.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:45):

Existential Delirium in the Evar Hell

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 14:45):

_fucked existential delirium fault_

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:45):

looks like a novel title

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:46):

We can go the medical way otherwise

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 14:46):

Existential Delirium in the Dereferencing Hell?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:46):

What about evarititis

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 14:46):

evaritis is good

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 14:46):

but Coq will still suffer from evarititis even after your PR

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:46):

It should go curing itself with the time

view this post on Zulip Matej Košík (Gitter import) (Mar 31 2017 at 14:47):

@Emilio Jesús Gallego Arias Bon chance!

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

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:47):

Yeah, we need an evarititis cure group

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 14:47):

@Matej Košík merci

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:47):

Did I already yelled enough at the world about how fucked up is Nsatz?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:47):

I've been rewriting it for the whole day. And yesterday also.

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:47):

Yes, but you should yell at the right person.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 14:47):

Not enough I'm afraid

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:47):

That's just beyond words.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:47):

I really need a therapy.

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:47):

https://coq.inria.fr/cocorico/CoqDevelopment/Maintainers

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:48):

Nah, it'll be faster to fix it myself

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:48):

I'm already done actually

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:48):

ok

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:49):

but by the god of specification

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:49):

If I had to grade this as a student work, it wouldn't pass

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

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:49):

At least make it a PR, so that he can see it.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:49):

How the hell did this get included in the repo?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:49):

Yes, I'm going to do a PR don't worry

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:49):

Inclusion of such low-quality code is the first thing we fixed.

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

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:50):

Basically we recently reduced the problem to a finite one...

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

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:51):

That should make you feel good

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:51):

@Matej Košík OK

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:51):

@Matej Košík Can you relauch it when you're done?

view this post on Zulip Matej Košík (Gitter import) (Mar 31 2017 at 14:51):

Ok. I'll do that.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:51):

thx

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

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:52):

You could think it was countable though, but I have doubts :)

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

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:53):

Oh by the way, what is the real answer to #526?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:54):

Deprecate Funind?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:54):

The argument of branch sharing does not make sense.

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

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:54):

constr

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:55):

Obviously constr. That's the only thing that has a canonical normal form.

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:55):

And even trickier, how does a plugin author make an informed choice?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:55):

Meh.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 14:55):

@Pierre-Marie Pédrot do you mean that glob_constr is redudant?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:55):

No, but it is an internal structure that you should not manipulate.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:56):

(Apart from producing it, storing it and pretyping it obviously.)

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

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

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:57):

Yeah... "On pousse mémé dans les orties"...

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

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:57):

No.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:57):

We need glob_constr, because that is the stable representation of data for storing.

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:57):

You should answer #526.

view this post on Zulip Maxime Dénès (Mar 31 2017 at 14:58):

It would be a start, to communicate.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:58):

It has all names resolved, which is important.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 14:58):

the stable representation of data for storing

sorry, storing what?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:58):

Glob_constr

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 14:58):

implicits arguments are better done in the syntax tree

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 14:58):

notations likewise

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 14:58):

in fact it is much better

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:58):

For instance when you have notations or ltac containing terms

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 14:58):

so that leaves us with name resolution

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:58):

the natural type you store is glob_constr

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

view this post on Zulip Matej Košík (Gitter import) (Mar 31 2017 at 14:59):

@Pierre-Marie Pédrot Done.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:59):

Well that's not any people.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 14:59):

well you could store constrexpr

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:59):

I mean they are somehow close to the dev team.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 14:59):

notations I'm pretty sure

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 14:59):

@Emilio Jesús Gallego Arias but you need names to be resolved

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 14:59):

things work much better if you resolved them over constrexpr

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:00):

and ditto for implicits arguments, the explicit application is there

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:00):

IDES would have a great time

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:00):

But that's not for ide

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

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:01):

It is like a compiled form of syntax.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:01):

bytecode if you want

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:01):

while constr is really the execution trace

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:01):

and constr_expr is raw syntax

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:01):

yeah I don't see the advantage of that

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:02):

other than creating a bit of chaos in the codebase

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:03):

and I'll bet it would actually clean up things a lot

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:03):

Don't forget the mighty funind plugin!

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:03):

I wish you luck to port that one

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:03):

in fact if you have a look to the code

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:03):

it is barely used

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:04):

You mean Function is barely used?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:04):

I mean glob_constr

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:04):

in fact PM is right, the main user is funind

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:05):

so indeed, funind either wants to work

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:05):

with constrexpr

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:05):

or with constr

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:05):

You still need to extend constrexpr a bit to replace glob_constr

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:05):

not with glob_constr

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:05):

right?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:05):

only for references?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:05):

the rest is there

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:05):

beware of the scope for tactic interpretation also

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:06):

and probably for arguments also

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:06):

so in the end you end up rewriting glob_constr i think

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:11):

anyways just a comment

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:11):

IMHO the issue is settles

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:11):

settled

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:11):

as it is really an internal thing

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:11):

and plugins should be forbidden to use glob_constr which I fully support

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:13):

in the sense

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:13):

it would be just adding 3 cases to the pretyper

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:13):

one for notations => call the notation compiler

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:13):

one for reference => call the reference solved

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:13):

one for impargs => call the impargs inserted

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 15:13):

inserter

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:17):

What do you mean?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:17):

It does what it should do.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:17):

nf_evar was doing that as well

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:24):

you mean whd_evar?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:25):

yep, that's the same

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:28):

Exactly.

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:29):

There would not be such things as 'Unsafe.to_univ'

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:29):

You mean it would be more helpful than for terms?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:29):

It would be helpful for terms as well actually.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:29):

We would probably save a lot of indirections.

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

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:30):

Yeah, so let's go step by step.

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

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:30):

(and then merge)

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:31):

Right.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:31):

What are the developments I should be looking at?

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:32):

HoTT is a special case, so we should not care too much at first.

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:32):

So we should start with HoTT. Verify your conjecture on universe normalization.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:32):

\o/

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:32):

Alternative facts FTW.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:32):

OK so what should I do?

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:33):

Ok, maybe, but couldn't universe normalization impact developments that don't use polymorphism?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:33):

May I extend the Constr.view term to account for universes as well?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:33):

Well, it does change the behaviour of Type-casing.

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:34):

There would be only two cases which are not identity : Evar and App.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:34):

Mhhh. Now that I'm thinking about it...

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:34):

There is a bug in EConstr.kind actually

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:35):

What is App doing?

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:35):

I'm realizing I forgot another case of smart constructors : Cast.

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:35):

Ah ah!

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

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

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:36):

Is the bug introduced only by your last commit?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:36):

No, it was there before.

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:37):

What does the Cast smart constructor do for two different kinds of Cast?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:37):

Eh...

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:37):

Who knows?

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:37):

Well, if we end up removing a vm_cast somewhere...

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:38):

So how about the following plan:

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:38):

  1. Revert the loop unrolling
  2. Fix the Cast bug
  3. Understand what are the slowest files in HoTT and the character theory.
  4. Perf the universe normalization on those two files.

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:39):

Very strange invariant.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:40):

What the hell is that supposed to mean?

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:41):

The treatment of Cast should be rewritten fully.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:41):

So? What do we ensure for EConstr casts?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:41):

Same as kernel?

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

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:42):

What do you think of my plan above?

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

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:42):

Yes

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:42):

LGTM.

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:42):

You can even add a technical note that it is probably broken for REVERTcasts...

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:47):

Do you need help somewhere in the plan?

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

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:53):

you can easily use the ci target for that

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:54):

make ci-hott

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:54):

and thank @Emilio Jesús Gallego Arias ;)

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:54):

Cool!

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:55):

Still, I'm finishing Nsatz up. I'm almost done.

view this post on Zulip Maxime Dénès (Mar 31 2017 at 15:56):

grrrrrrrrrr

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 15:56):

If you guys stop distracting me sending messages. The notification thingy is really disturbing.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 16:30):

@Pierre-Marie Pédrot disable it; I've done so indeed

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

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 22:58):

Luckily, almost nobody relies on this as of today, except people doing universe polymorphism.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:25):

O_O

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:27):

How much fun!

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 23:28):

It's Friday, Friday, Friday, gonna get fun fun fun...

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:31):

Never had a Friday like this

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:32):

of course, purely imperative programming couldn't be far from my fun

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 23:32):

Chasing bugs on Friday night is a well-known practice!

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:32):

in this particular case, we are talking about _purely imperative error handling_

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:33):

ok got it: purely imperative programming, case 2 vs expected case 0

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 23:33):

Come on, the EXTASIS of finding that $%!§£ universe leak...

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:34):

"extasis" falls short of describing what you can feel

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 23:34):

Not close to it yet unluckily.

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:35):

and would likely be cleaner

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:38):

well, I sadly need to go back to my .tex files

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 23:38):

Good luck...

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:39):

Thanks PM!

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 23:40):

Yeah, I wrote Exninfo.add.

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:45):

Here you have it.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:45):

Lots and lots of imperative fun

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:46):

You got me =>

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:47):

however Exninfo.add has been badly abused in the STM

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 23:47):

Well, the original implementation, believe me or not, was pure;

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 23:47):

Unluckily, it relied on OCaml < 4.01 representation of exceptions

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 23:48):

and used unsafe machinery to mangle exceptions.

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:49):

people^W the STM

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:49):

in fact yeah it seems badly broken

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 23:50):

now that we have PPX we may try do that by using a wrapper

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 23:50):

ensuring that all try / with are guarded

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:50):

what about doing external reraise : exn -> 'a = "%reraise"

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:50):

?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:51):

oh well you mean for catchable ones, that would be fine

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 23:51):

this needs to ensure that no exception was raised in the meantime

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

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2017 at 23:54):

I never got the whole stuff about exception wrapping in the STM

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2017 at 23:58):

I see

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2017 at 00:00):

thx

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2017 at 00:02):

So would you support a change towards type iexn = exn * Backtrace.t ?

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2017 at 00:03):

You may want other irrelevant information than Backtrace, e.g. locations.

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

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2017 at 00:04):

That is only for debug or printing.

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2017 at 00:09):

but yeah that is very low priority

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2017 at 00:09):

the stm stuff is of higher priority thou

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2017 at 00:10):

Do as you prefer, I can't say I'm fond of this code.

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2017 at 00:22):

Aha! Got my bug.

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2017 at 00:30):

:D seems a bit like a chicken and egg problem :D

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2017 at 00:31):

It's a miracle that Coq is not yet bootstrapped.

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

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2017 at 00:32):

In ye olde days, we were cowboys !

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

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

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2017 at 00:47):

Working on it.

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2017 at 00:47):

I've already stopped normalizing universes, and on my way to instances.

view this post on Zulip Maxime Dénès (Apr 01 2017 at 00:47):

but you do that by implementing the lazy universe normalization?

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2017 at 00:47):

Yes.

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2017 at 00:47):

This is always going to be more efficient.

view this post on Zulip Maxime Dénès (Apr 01 2017 at 00:47):

I would have used a profiling tool.

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2017 at 00:48):

Even for non-universe polymorphic code.

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

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2017 at 00:48):

For now, this looks OK.

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

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

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2017 at 00:49):

Finger in the gear, they say...

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

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2017 at 00:50):

I'm really sure this is because of that.

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

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

view this post on Zulip Maxime Dénès (Apr 01 2017 at 00:52):

I'm only a second couteau in this stuff, but I have no mercy.

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2017 at 00:52):

And need no sleep, I see

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2017 at 01:10):

Maxime stop interrupting PM, he's trying to work !

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2017 at 05:04):

We should get @herbelin here

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2017 at 05:04):

I think he's the one that may know, maybe Matthieu too?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2017 at 05:05):

I guess @Théo Zimmermann can lure him in

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

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

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

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

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

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

view this post on Zulip Théo Zimmermann (Apr 01 2017 at 16:28):

@Pierre-Marie Pédrot I'd be interested in your config line.

view this post on Zulip Théo Zimmermann (Apr 01 2017 at 16:29):

cool thanks!

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2017 at 16:29):

The important line is the third one.

view this post on Zulip Théo Zimmermann (Apr 01 2017 at 16:34):

yeah I figured out (after some comparison to existing configuration)

view this post on Zulip Théo Zimmermann (Apr 01 2017 at 16:48):

I wonder if there is a way to see only opened PRs

view this post on Zulip 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? ¯\_(ツ)_/¯

view this post on Zulip Théo Zimmermann (Apr 01 2017 at 17:31):

Thanks @Jason Gross! That's quite useful information.

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

view this post on Zulip Théo Zimmermann (Apr 01 2017 at 18:15):

this will avoid me fetching too many PRs

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

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2017 at 18:26):

AFAICT HoTT still compiles, which is a good thing...

view this post on Zulip Maxime Dénès (Apr 01 2017 at 20:07):

@Pierre-Marie Pédrot Nice! Let me know how it goes.

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2017 at 20:08):

pendulum is a bit crowded at the time...

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

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2017 at 20:09):

in ./src/WeierstrassCurve/WeierstrassCurveTheorems.v

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

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

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

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

view this post on Zulip Jason Gross (Apr 01 2017 at 21:50):

@Pierre-Marie Pédrot Nice!

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

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

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

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

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

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

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

view this post on Zulip Matej Košík (Gitter import) (Apr 02 2017 at 18:15):

@Jason Gross yes and yes.

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

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

view this post on Zulip Pierre-Marie Pédrot (Apr 02 2017 at 18:23):

OK, thanks, I'll retry a bench for EConstr.

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

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

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

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 02 2017 at 23:38):

Note also the mz-8.7 branch

view this post on Zulip Emilio Jesús Gallego Arias (Apr 02 2017 at 23:38):

which is the one used for trunk

view this post on Zulip Emilio Jesús Gallego Arias (Apr 02 2017 at 23:39):

we should eventually get to integrate that one, but not urgent IMO.

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 02 2017 at 23:40):

[for travis] that will solve the dpdgraph problem

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

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

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

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

view this post on Zulip Jason Gross (Apr 03 2017 at 00:31):

@Emilio Jesús Gallego Arias Thanks for the pointer re HoTT

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

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

view this post on Zulip Jason Gross (Apr 03 2017 at 00:35):

Why this makes Defined take forever, I don't know

view this post on Zulip Jason Gross (Apr 03 2017 at 00:35):

(see https://coq.inria.fr/bugs/show_bug.cgi?id=5437 for more details)

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

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

view this post on Zulip Jason Gross (Apr 03 2017 at 00:37):

*and T3 is of the form

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

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

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 11:54):

Why not? Last time I tried it worked...

view this post on Zulip Maxime Dénès (Apr 03 2017 at 11:56):

Because we broke Flocq

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

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 11:57):

and it got merged.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 11:57):

oh!

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 11:58):

AFAIK, there is no opam package.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 11:58):

@Pierre-Marie Pédrot what is the status of EConstr?

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 11:58):

Waiting for a bench on HoTT

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 11:59):

I'm expecting time gain for everybody (hopefully).

view this post on Zulip Maxime Dénès (Apr 03 2017 at 11:59):

What build is it on Jenkins?

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 12:00):

#102

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 12:03):

Ok I'll interrupt it.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 12:05):

We should put only one iteration for benchmarks

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 12:05):

All right, I thought 3 was coming from some rule of thumb.

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 12:06):

Should we ensure master is merged before benching then?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 12:16):

No, precisely if you do that you'll run into trouble.

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 12:16):

You may be comparing two unrelated branches...

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 12:22):

Fine, I'm leaving the dirty work to you for now then.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 12:26):

@Maxime Dénès Should I perfom a merge into EConstr anyway?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 12:40):

I did it recently, so it won't change much

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 12:42):

That's probably unsound now that we removed eager normalization.

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 12:42):

It probably still is in EConstr, though a bit less.

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

view this post on Zulip Enrico Tassi (Apr 03 2017 at 12:43):

wouldn't that be sound?

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 12:43):

Probably not anyway.

view this post on Zulip Enrico Tassi (Apr 03 2017 at 12:43):

would it be less sound than without econstr?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 12:44):

Well, I don't think we can measure things like that.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 12:44):

I'd say on the same order of magnitude.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 12:44):

Fact is, nobody is using universe polymorphism.

view this post on Zulip Enrico Tassi (Apr 03 2017 at 12:44):

I mean: more bugs, same bugs, different bugs

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 12:44):

Except crazy people who don't care yet about another buggy unification

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 12:45):

+1

view this post on Zulip Maxime Dénès (Apr 03 2017 at 12:45):

(in the few developments that actually use univ poly)

view this post on Zulip Enrico Tassi (Apr 03 2017 at 12:45):

I still don't get where the change would come

view this post on Zulip Enrico Tassi (Apr 03 2017 at 12:45):

from

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

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

view this post on Zulip Enrico Tassi (Apr 03 2017 at 12:47):

sorry, I did not make the context of my question clear

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 12:48):

@Enrico Tassi I don't believe this is feasible.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 12:48):

well the question is: with how much code duplication?

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 12:48):

Yeah obviously you can duplicate all folders starting from engine

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 12:49):

We don't want to do that, do we?

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 12:49):

it is so broken!

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 12:50):

Welcome in Coq Hell, Mr Anderson.

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

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 12:51):

it is an interesting and underdocumented issue

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 12:52):

I already forgot. How can we find something in the history of the chat?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 12:52):

"Search Gitter" in the leftside panel

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 12:54):

@Enrico Tassi I started to do that for real

view this post on Zulip Enrico Tassi (Apr 03 2017 at 12:54):

... and...

view this post on Zulip Maxime Dénès (Apr 03 2017 at 12:54):

I can show you the code, I gave up after two days of work

view this post on Zulip Maxime Dénès (Apr 03 2017 at 12:55):

and like 10+ hours each day sitting at the desk

view this post on Zulip Maxime Dénès (Apr 03 2017 at 12:55):

I got something that compiled and failed on the stdlib...

view this post on Zulip Enrico Tassi (Apr 03 2017 at 12:57):

so which is the future of econstr?

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 12:57):

@Enrico Tassi I'd favour merging and seeing if we broke things.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 12:57):

more precisely, we fixed the last known incompatibilities

view this post on Zulip Maxime Dénès (Apr 03 2017 at 12:58):

now we'd like to fix the performance overhead

view this post on Zulip Enrico Tassi (Apr 03 2017 at 12:58):

this branch includes the removal of some nf_evar, fixes to pretyping, ...

view this post on Zulip Enrico Tassi (Apr 03 2017 at 12:58):

all that?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 12:58):

yes

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 12:58):

It's very intricate, I agree.

view this post on Zulip Enrico Tassi (Apr 03 2017 at 12:59):

well good luck

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

view this post on Zulip Enrico Tassi (Apr 03 2017 at 12:59):

I only partially agree, IMO you did look for troubles ;-)

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 13:00):

I think we really had to do this at some point.

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 13:02):

I'm not sure I'm willing to answer the discussion on funind actually...

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 13:04):

Let them merge their code, and at some point kick funind out the repo.

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 13:25):

If I can put a bit more argumentation on the table:

view this post on Zulip Théo Zimmermann (Apr 03 2017 at 13:29):

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

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

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

view this post on Zulip Théo Zimmermann (Apr 03 2017 at 14:33):

Yes, I suppose the same fate awaits the unification of the unification algorithms.

view this post on Zulip Théo Zimmermann (Apr 03 2017 at 14:34):

Although, this could happen in a later release.

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 14:35):

@Matej Košík WTF? Isn't HoTT in the default packages for the bench?

view this post on Zulip Théo Zimmermann (Apr 03 2017 at 14:36):

Already! Great news. Where did he found the money for it?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 14:36):

I'm wasting my time waiting for the bench since hours.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 14:36):

I don't know, I wasn't involved in the hiring process

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

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 14:50):

But indeed it is always good to get more manpower, we badly need it.

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

view this post on Zulip Matej Košík (Gitter import) (Apr 03 2017 at 15:29):

@Pierre-Marie Pédrot That's what we did. Intermediate results:


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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 15:32):

Well, there were quite a few other packages in the run, weren't there?

view this post on Zulip Matej Košík (Gitter import) (Apr 03 2017 at 15:35):

Benchmarking was finished only for two packages:

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 15:36):

All right then. That's slow as hell for two packages...

view this post on Zulip Matej Košík (Gitter import) (Apr 03 2017 at 15:39):

-j1 :-(

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 15:40):

And luckily intuitionistic-nuprl is not in there!

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

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

view this post on Zulip Enrico Tassi (Apr 03 2017 at 16:32):

I guess we all need a candy before going home...

view this post on Zulip Enrico Tassi (Apr 03 2017 at 16:32):

Check forall x : nat, forall x : Prop, x -> x.

view this post on Zulip Enrico Tassi (Apr 03 2017 at 16:33):

nat -> forall x0 : Prop, x0 -> x0

view this post on Zulip Matej Košík (Gitter import) (Apr 03 2017 at 16:33):

@Pierre-Marie Pédrot That makes sense.

view this post on Zulip Enrico Tassi (Apr 03 2017 at 16:33):

;-)

view this post on Zulip Matej Košík (Gitter import) (Apr 03 2017 at 16:33):

... makes sense

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 16:33):

LGTM. Where is the trick?

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 16:34):

@Matej Košík Fine for me.

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

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 18:26):

@Maxime Dénès The bench did not use the right branch for mathcomp :/

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

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

view this post on Zulip Matej Košík (Gitter import) (Apr 03 2017 at 21:01):

@Maxime Dénès Tomorrow I'll try to implement them.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:02):

Great! We can discuss it a bit, it requires a bit of design.

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:03):

oh ok, thanks! So that's what Jenkin's \#26 is doing?

view this post on Zulip Matej Košík (Gitter import) (Apr 03 2017 at 21:03):

Yes.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:04):

Sounds very good, thanks.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:04):

@Pierre-Marie Pédrot What do you think of HoTT's timings?

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 21:05):

They look OK.

view this post on Zulip 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 % │
└─────────────────┴─────────────────────────┴─────────────────────────────────────┴───────────────────────────────────────┘

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 21:05):

I think we're close to merging EConstr, aren't we?

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

view this post on Zulip Matej Košík (Gitter import) (Apr 03 2017 at 21:06):

(but anyway, without those "overlays" wouldn't provide more results)

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:06):

You'll need to convince everyone ;)

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 21:07):

Come on, that's coq-hott.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:07):

You should draw a chart performance x correctness

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 21:08):

We need an axis about program proof...

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 21:08):

It's possible to have full performance at the expanse of proving your code!

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:08):

Proofs are overrated.

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:09):

WDYM?

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 21:09):

For instance, some kind of imperative but persistent representation.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:09):

oh yes

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:10):

didn't they use to have that in like Coq 4?

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 21:10):

So that one does evar normalization literally only once.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 21:10):

No idea, I can have a look

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:10):

Maybe it was not for evar or meta substitution

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 21:10):

that'd be @Emilio Jesús Gallego Arias's sweet dream

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:10):

but I've heard one day about an imperative data structure for Coq terms

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:11):

don't know if it was a legend

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 21:11):

Coq source code. A time of legend and heroes

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:11):

That would make a great movie.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 21:11):

a horror movie most probably

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:12):

nope, not for trunk

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:13):

oh no, that's a different one

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

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

view this post on Zulip Matej Košík (Gitter import) (Apr 03 2017 at 21:16):

Anyway, you can see my modification on pendulum...

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:18):

Yeah you added the repo instead of replacing it...

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

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:22):

It doesn't work because it fetches mathcomp from coq-extra-dev.

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:23):

I don't know, but why keep coq-extra-dev?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:25):

I adjusted it.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:25):

Can you launch a last one?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:25):

Maybe it will run over night this time.

view this post on Zulip Matej Košík (Gitter import) (Apr 03 2017 at 21:25):

Done. Let's see...

view this post on Zulip Maxime Dénès (Apr 03 2017 at 21:29):

I saw you solved the issues, sounds very good.

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 22:19):

@Matej Košík git show 4f041384cb27f0d24fa14b272884b4b7f69cacbe kernel/nativecode.ml

view this post on Zulip Matej Košík (Gitter import) (Apr 03 2017 at 22:20):

?

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 22:22):

Shitstorm in approach!

view this post on Zulip Maxime Dénès (Apr 03 2017 at 22:22):

That's what causes https://coq.inria.fr/bugs/show_bug.cgi?id=5435

view this post on Zulip Maxime Dénès (Apr 03 2017 at 22:23):

So? Any player?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 22:24):

hint: the first let-in was there for a reason

view this post on Zulip Maxime Dénès (Apr 03 2017 at 22:25):

let's make it a proof of false

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 22:26):

There are suspicious discrepancies.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 22:26):

I wouldn't be surprised...

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 22:26):

Actually I'm hoping to give static invariants to it

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 22:26):

by carefully chosing datatypes, and encoding info in GADTs

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 22:26):

nah

view this post on Zulip Maxime Dénès (Apr 03 2017 at 22:27):

hmmm

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 22:27):

You need to be inside a term for it to be non-empty.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 22:27):

I think.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 22:27):

yeah but fortunately I have native casts

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 22:27):

\o/

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 22:27):

Fortunately.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 22:28):

That's what you get for trusting native_compute.

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 22:29):

What about my PR touching the kernel btw?

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 22:30):

I'm pushing for the swift integration of the array mapping one !

view this post on Zulip Maxime Dénès (Apr 03 2017 at 22:31):

Was there any complaint?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 22:31):

I'll read again

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 22:31):

I think @silene complained about the ugliness.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 22:31):

Let me finish my proof of false. I put too many assertions...

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:01):

So, is Coq 8.6 inconsistent?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:11):

Hmm I don't understand why my term doesn't type check

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:11):

Maybe you can help me:

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:11):

Definition foo (T := False) (U := T) (x : True) (X := True) := x <<: U.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:11):

Lemme see

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:12):

How does the typechecker know I'm trying to make fun of him?

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:12):

He's reached self-consciousness

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:13):

In fact, when I use the cast, two type checks are triggered

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:13):

I don't understand where this second check comes from.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:14):

backtraces to the rescue!

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:15):

Yeah I looked at it already.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:18):

I get fancy assertion failures if I play a bit with the term.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:18):

We're walking on thin ice!

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:18):

Yeah but those are "expected" given the bug.

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:21):

Interesting:

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:23):

I don't understand how definitions are type checked...

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:24):

I also get a few stack overflows

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:25):

did you make sense of the backtrace on my initial example?

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:25):

Not quite, I'm launching a debugger to see what happens

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:26):

the other errors you see are probably at reification time

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:26):

but my example is cooked up to make the thing go through

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:26):

All right.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:27):

how do we go from term_typing to fast_typeops?

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:28):

I think I got it.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:28):

tell me :)

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:28):

is native compilation enabled by default ?

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:28):

I think not

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:28):

it falls back to VM right?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:28):

Yes it is enabled by default.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:28):

sure ?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:29):

Sure. What is not enabled is the precompilation except for stdlib.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:29):

And tests are running, I saw the generated code.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:29):

cause the native conversion fails in the cast

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:29):

From what I saw, it is called twice.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:29):

The first time it succeeds, the second time it fails.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:30):

yep

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:30):

same behaviour here

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:30):

But I don't understand the second call.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:30):

Also, why don't we see something related to native_compute in the backtrace?

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:30):

nah, that's because the trace is not propagated

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:31):

What does that mean? I'm always confused when trying to debug.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:31):

Where is it not propagated?

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:31):

one need to add some CErrors.push to Typeops.check_cast

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:32):

check_cast?!

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:32):

yep

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:32):

There is no check_cast in 8.6.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:32):

oh, I'm on trunk

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:32):

but that should be the same

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:33):

The hell are we doing in the stm

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:34):

something is wrong

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:34):

yeah I don't understand

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:35):

the second time?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:35):

yeah of course

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:35):

it's being asked to compare True and False

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:35):

obviously

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:35):

but the question is who called it?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:36):

I may be blind, but I don't see what typing rule does that.

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:36):

so the native compiler is asked to compare

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:37):

Ah yeah

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:37):

Where are the casts gone?!

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:38):

no, we're checking the cast

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:38):

Oh!

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:38):

isn't that supposed to be the same because of your bug?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:38):

Well it depends. I thought what we were doing

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:39):

Erm...

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:39):

isn't that because of this implementation ?

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

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:39):

hum

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:39):

we abstract over the context

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:39):

I'm too paranoid.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:40):

so, no soundness bug?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:40):

But then who makes the first call?

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:40):

the environment is wrong that said

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:41):

The first call produces wrong code, I checked.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:41):

Nah, in trunk there is only one call which is NativeCast

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:41):

Yeah but probably there is one in the pretyper.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:41):

I got it know.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:41):

?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:41):

Hum not quite.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:42):

In 8.6, I can swear the compiler is called at least twice.

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:42):

I see the generated code.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:42):

I can check if you want

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:42):

The first time it is incorrect, the second time it is correct.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:43):

clearly the code has changed between trunk and 8.6

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:43):

let me try in trunk

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:44):

still two calls

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:44):

probably with different environments

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:45):

can't reproduce on trunk

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:45):

if you do -debug

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:45):

you can look for .native files in /tmp

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:45):

I'm in the debugger, this does not work

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:46):

nah, in 8.6 only one native cast as well

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:46):

I'm using bytecode so I'm not sure what is supposed to happen

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:47):

probably

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:48):

can you try in native?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:48):

so what you get in /tmp

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:48):

see*

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:48):

lemme try

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:48):

independently of the soundness

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:48):

What should I observe?

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:48):

I can observe the backtrace if you want

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:49):

each conversion test leaves a xxxxx.nativefile in /tmp

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:49):

my example creates at least two on my machine

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:49):

you can open them, they are ml source files

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:50):

I'll tell you right now

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:50):

I only get one call to nativeconv

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:50):

and you see only one file?

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:51):

I get two

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:51):

WTF did I mess up?

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:51):

no wait

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:51):

I get none actually

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:51):

there is indeed a compiled cmxs / o whatever

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:51):

if you don't put -debug, they don't stay

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:52):

but no native

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:52):

ah ok

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:52):

Ok

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:52):

in debug mode, I do get two calls to native compilation

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:52):

and thus two files !

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:52):

what?!?!

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:52):

isn't that some stm story?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:52):

only in debug mode?

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:52):

about backtrack blahblah

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:52):

yep

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:53):

but it's not even the same environment

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:53):

who knows

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:53):

something bad is going on

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:53):

First backtrace:

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:53):

argh no

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:54):

that's the backtrace of the error sorry

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:54):

but I do get two files

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:54):

strace to the rescue

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:54):

so maybe that is independent from the debug mode, right?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:55):

I have a feeling I screwed up something myself here ^^

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:55):

Yeah, right, I get 2 cmxs even without debug

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:55):

but I have no idea what

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:55):

I can look at who opens a file

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:56):

well

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:56):

it is native_conv

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:56):

so the only missing bit is to find the two calls

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:56):

no, I'd see the other trace

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:56):

at least it's not Nativeconv.native_conv

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:56):

maybe native_conv_gen, let me check

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:56):

native_conv_gen?

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:56):

yeah

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:57):

it would explain why it's not abstracted...

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:57):

this part is terrible, I'm ashamed

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:57):

indeed

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:57):

"used outside of the kernel"

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:57):

says the comment :)

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:57):

Rhat

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:57):

it does not fit

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:57):

let's split them

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

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:58):

Then

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

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:58):

yeah sorry, I understand now

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:58):

so reductionops is calling it

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:58):

there is an infer_conv for native

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:59):

to infer univ constraints and so on

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2017 at 23:59):

ah!

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:59):

I had forgotten about that

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:59):

before universes there was only one conv function

view this post on Zulip Maxime Dénès (Apr 03 2017 at 23:59):

and one for normalizing

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

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:00):

yep !

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:00):

once again, doubling everything saves the day

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:00):

it is probably more efficient to do it

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:00):

but I was scared to remove it from the kernel

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:00):

well in that case the kernel was right

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:00):

but just in case you never know

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:00):

I mean more efficient not to do it

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:00):

yeah

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:00):

not that the passed environment is still wrong

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:00):

really?

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:00):

I don't think there is a way to work around that

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:01):

yes, if you abstract over it

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:01):

you should clear the rel context

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:01):

oh yes

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:01):

I don't think you can exploit that but still

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:01):

but it's unused then

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:01):

I agree it's not pretty

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:01):

I'm always afraid about universe constraints

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:01):

also we compile a lot of useless stuff

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:01):

couldn't you get a leak by duplicating the relcontext?

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:02):

I have no idea.

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:02):

speaking about which, did you have a look at malfunction in the end?

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:02):

not that I remember

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:03):

did you talk to me about it? :)

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:03):

I forget things these days

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:03):

yep I did !

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:03):

that's just an API over dlambda

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:03):

probably better than spitting Obj-ified ML code

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:03):

I see, that sounds nice.

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:03):

since we're in OCaml 4.02...

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:04):

But how good is it to depend on it?

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:04):

well, that's a very small wrapper

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

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:04):

I'm not sure about how stable dlambda is

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:04):

Hum

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:04):

"Malfunction is released under the same terms as OCaml."

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:04):

the subset you use is small

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:05):

well, we could recode it

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:05):

oh but it's LGPL now?

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:05):

yeah, how juridically clear is native_compute BTW ?

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:05):

it is very clear!

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:05):

much clearer than EConstr!

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:05):

LGPL 2.1

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:05):

what?

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:06):

The Great Proud University of Ljubljana

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:06):

has now shares in Coq

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:06):

BEHOLD

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:06):

First, American first lady

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:06):

now: Coq

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

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:07):

« c'est comme d'habitude : le gouvernement niera avoir eu connaissance... »

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:07):

LGPL, dude

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:07):

that's like we're gangsta

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:07):

no liability whatsoever

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:08):

still, I think it would be worthwile to plug directly into dlambda

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:08):

I'll give Matej's name :)

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:09):

what we should do is remove all this

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:09):

and implement Coqonut!

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:09):

?

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:09):

well, you could probably remove coq altogether

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:09):

and use LEAN

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:09):

that's C++

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:09):

safest of the safest

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:09):

look ma, no garbage collection

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:10):

they don't need to, they don't allocate arrays like crazy :D

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:10):

I'm waiting for the implementation of Coqonut

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:10):

Tomorrow by 2pm, is that possible?

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:10):

OP delivered EConstr

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:11):

Tomorrow is the day of insensitivity

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

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:11):

do we have some mathcomp results?

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:12):

Seems to be a failure

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:12):

oh but of course

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:13):

we didn't port it to EInstance

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:13):

I mean you didn't do it!

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:13):

Too busy finding bugs in universes

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:13):

and rewriting the kernel

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:13):

and universe unification

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:13):

and nsatz

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:14):

Ok, so let's do that tomorrow.

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:14):

fine

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:14):

I think I'll go to bed

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:14):

Meanwhile, enjoy the night, and thanks for your help!

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:14):

you're welcome

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:14):

I'm always interested in finding soundness issues

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:14):

did you know we got cited in SIGBOVIK last year for that?

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:15):

lol really?

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:15):

yep

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:15):

http://sigbovik.org/2016/proceedings.pdf

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:17):

UNPRL: NUPRL PROOF RE-EVALUATION LOGIC

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:17):

yeah I read

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:18):

not sure it is the best way to become famous :)

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:18):

That's international fame come on

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:18):

probably my best citation up to no

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:18):

*w

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:18):

The ultimate SIGBOVIK 1 H-index

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:19):

I should probably get some sleep

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

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:19):

and some cheese

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:19):

in an indistinct order

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:19):

nobody cares

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:19):

you can die for their freedom

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:19):

this is AMERICA

view this post on Zulip Maxime Dénès (Apr 04 2017 at 00:19):

yep, see you tomorrow for more bugs and more fun

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 00:19):

see you then

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2017 at 01:35):

using opam to do benchmarking is like using NUPRL to make foie gras

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

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

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 10:08):

https://github.com/PrincetonUniversity/VST

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 10:08):

Theoretically HEAD compiles both with 8.6 and trunk.

view this post on Zulip Matej Košík (Gitter import) (Apr 04 2017 at 10:38):

@Pierre-Marie Pédrot Ok. I am on it.

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

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 11:44):

@Matej Košík Thanks a lot!

view this post on Zulip Matej Košík (Gitter import) (Apr 04 2017 at 11:52):

@Pierre-Marie Pédrot You are welcome.

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2017 at 12:09):

@Jason Gross sure, let us know where the code is

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

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

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

view this post on Zulip Maxime Dénès (Apr 04 2017 at 14:53):

Yeah I'm working on it. We need to merge trunk into econstr.

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 15:34):

Can I play with pendulum or should we bench EConstr first?

view this post on Zulip Matej Košík (Gitter import) (Apr 04 2017 at 15:36):

@Pierre-Marie Pédrot I am not doing anything there, right now...

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 15:36):

@Maxime Dénès ?

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

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:02):

Well, that's not a huge amount of memory, is it?

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

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

and it is relatively compact

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:03):

Modules are known to be costly. Even the vo files are big.

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:03):

Not mentionning the vio.

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

yeah I see

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

they have some non-linear growth factor it seems

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:04):

You can use votour on the vio if you want to have an idea

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:04):

yes, everything is duplicated when applying a module substittuion

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:05):

AFAIR, the problem stems from the field Declarations.mod_type.

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:05):

We ought to keep it abstract, but we expand it unconditionally, and bam.

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

maybe it is the time to increase the density parameter of Coq

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:11):

?

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

to stop it expanding I mean

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

I guess that making mod_type abstract is science fiction material, right?

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:12):

That's worse, I'm not sure why it would make sense.

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:13):

How making it abstract would sove the issue?

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

Oh no clue myself, you had mentioned it

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:13):

ah yeah, I misunderstood your statement

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:14):

Abstract as in Coq, not as in OCaml

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:14):

Well, I have no idea of the feasability

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:14):

And the worst thing is that probably nobody has.

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

I see, thanks

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:14):

Because you know, modules.

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

Yeah, modules are really opaque to me

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

the way the obj system is organized, hard to dwell in

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:15):

Obj system is not that bad.

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:15):

You have to understand when the methods are called but that's about it.

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:16):

Modules are really intricate, OTOH.

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

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

like let's say, from SerAPI

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:17):

That's the wonder of existential types.

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:17):

You could add a marshalling method if you like.

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:18):

That's not very hard actually.

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

all the subst_object stuff

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

yeah it is not hard

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

but incovenient

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

I am not a fan of such "generic" stuff

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:18):

Coq needs to be extensible, if you want to write e.g. plugins.

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

extensible != generic stuff

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:19):

What do you call generic?

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

libobject

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

contains very different objects

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

with very different API

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:20):

You don't like OOP?

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

also the way classification works

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

totally hinders following the data flow scheme

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

it is a matter of responsibilites

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

the module system should take of the disposal

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

explicitly

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

when closing modules etc

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:20):

I agree that it would be better to have inversion of control

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

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

indeed

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

you could of course, provide a proper extension API for the enviroment, etc...

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:21):

If you start writing purely functional interface to libobject

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:21):

that should become possible

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:22):

I'm actually not sure this is that hard in the end.

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:22):

We can always write imperative wrappers in the transition phase.

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

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

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

but anyways it was just a comment

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

how would such interface look like in your opinion PM?

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:24):

I'd say that there is a blobby State.t

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:24):

where you can add you own stuff.

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

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:25):

or

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:25):

more precisely

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

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:26):

we can probably do that with GADTs.

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

should that be merged with summary ?

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

I'd say so

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:26):

Well there would not be a real need of summary afterwards

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

that's something worthwhile to pursue

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:27):

yep

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

the key question is what the structure of State.t should be

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

indeed you have proof state, section state

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

somehow you would like to expose the section org

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

Something we have problems handling in the stm indeed is sectioning and modules

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:30):

There are fishy things in the kernel about both sections and modules anyway

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

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 16:36):

That includes EConstr :bomb:

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

:shipit:

view this post on Zulip Maxime Dénès (Apr 04 2017 at 18:27):

@Pierre-Marie Pédrot I'm not far

view this post on Zulip Maxime Dénès (Apr 04 2017 at 18:27):

can you make the list?

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

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 18:30):

#400 : @Matthieu Sozeau happy but not @silene

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 18:30):

#508 : seemingly uncontroversial

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 18:31):

#519 : @Enrico Tassi complaining, but off-topic I think

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 18:31):

and then a few more which need more testing and discussion.

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 18:34):

ah and obviously :

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 18:34):

#379 : the one PR to rule them and and in insensitivity bind them

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2017 at 19:24):

Also, is there a possibility that #434 / #400 may affect adversely flambda ?

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 19:24):

#434 is independent from Flambda AFAICT.

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

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 19:26):

Thankfully we can bench!

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2017 at 19:26):

well yeah maybe we should test

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2017 at 19:27):

so we could define #OPTIM

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

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 19:28):

We can do that with a PPX

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 19:29):

and by the miracle of OCaml 4.02 we do have ppx around

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2017 at 19:32):

so I fear adding #ifdefs to Coq

view this post on Zulip Matej Košík (Gitter import) (Apr 04 2017 at 19:54):

@Emilio Jesús Gallego Arias No.

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

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

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:07):

@Pierre-Marie Pédrot hum, what is happening again?

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:07):

Where?

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:08):

on pendulum

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:08):

Ah! I don't know.

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:09):

This machine seems a bit capricious if you ask me

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

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:13):

I don't understand why it failed

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

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:16):

Wait this did not get merged yet?

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:16):

I thought I had merged it precisely before launching this build.

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:17):

Let me try with a more specific commit sha1.

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:17):

Oh but I see!!

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:17):

I didn't merge ssr's fix to my econstr branch. I'm stupid.

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

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:19):

I want math-comp:master, and didn't ask for anything

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:22):

Yeah the script has been hijacked for that.

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:22):

Grrr

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:22):

Because overlays are being implemented by @Matej Košík.

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:22):

Did you see #539?

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:23):

Like I have time to read other's PR

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:23):

I'm writing them sir

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:24):

Oh, that's just like 6 minutes ago

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:24):

I was wondering why I hadn't seen it

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

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:25):

But we surely need to merge EConstr before this :)

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:25):

I'm hoping for the removal of unification though

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:26):

removal of unification = removal of apply

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:27):

yeah, nice equation

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:27):

I'm in, where do I have to sign?

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:27):

so removal of unification means new tactics

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:27):

at least for apply

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:28):

now the question is, why reimplement one that is different from ssr's apply?

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:28):

I don't care, just want unification.ml gone

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:29):

do you happen to know how to time HoTT?

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:29):

I'm using the timing-html target, but I get a too detailed result

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

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:29):

sorry, I don't know

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:29):

Any path is good

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:30):

What about my PRs?

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

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:30):

(this does not include EConstr)

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:30):

ok, here is one thing I need to understand

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:30):

is there a chance that they are subsumed by flambda?

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:31):

I'd say only #400 potentially

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:31):

the array mapping is untouched by Flambda AFAICT

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:32):

and the others are not micro optimizations

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:32):

they're real algorithmic reworking

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:32):

ok, let me review briefly and merge #434 now

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:33):

A few of the PR can be considered as bugfixes for 8.6

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:34):

ah ah!

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:34):

which one for instance?

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:35):

#537

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:35):

A part of #532

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:35):

(which I can extract)

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:35):

Oh, I missed that one because it was not in your list.

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:36):

#519

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:36):

Ok, I'll merge #434 in trunk first.

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:36):

Probably not all of #519 because it changes the representation of summary

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:37):

yay!

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

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

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:42):

WDYM concretely?

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:42):

There is a huge portion of the time spent in hashconsing of universes

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:42):

We can deactivate it

view this post on Zulip Maxime Dénès (Apr 04 2017 at 23:42):

lol

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:42):

and trick them into believing EConstr is faster

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

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:43):

@Jason Gross you didn't hear anything

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:43):

That's a one-line change

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:43):

I can submit a PR

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

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

view this post on Zulip Pierre-Marie Pédrot (Apr 04 2017 at 23:45):

Fine with me.

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

view this post on Zulip Maxime Dénès (Apr 05 2017 at 05:56):

@Matej Košík sounds good!

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

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

view this post on Zulip Maxime Dénès (Apr 05 2017 at 08:19):

@Matej Košík ok, thanks!

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2017 at 12:04):

Oh sure, I'd be great to converge

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

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

view this post on Zulip Maxime Dénès (Apr 05 2017 at 12:29):

Sure!

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

view this post on Zulip Pierre-Marie Pédrot (Apr 05 2017 at 12:37):

Isn't there already such a thing? It rings a bell.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2017 at 12:37):

only for native compute

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2017 at 12:37):

AFAICT

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

view this post on Zulip Pierre-Marie Pédrot (Apr 05 2017 at 12:40):

Well, that looks useful.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2017 at 12:41):

yeah my original plan was to port