Stream: Dune devs & users

Topic: Coqdep vs. Coqmod


view this post on Zulip Rudi Grinberg (Jun 11 2022 at 16:25):

Regarding the recent impasse with coqmod vs coqdep, I have an idea that might let us side step all these issues. To summarize the current problem:

On one hand, we need an improved dependency analysis tool to improve's dune support for coq. On the other hand, we don't want to dump an independent tool into the coq repo that's duplicating half of what coqdep is already doing.

Each side brings valid points:

Basically, there seems to be no way to keep both sides happy. So how about this compromise:

We start the development of coqmod in dune itself. There we can modify it rapidly to meet dune's needs without disturbing anyone. Once we're confident about the implementation (we can at least build the coq-universe with it), we can submit a proposal for official inclusion in coq. At that point, we should of course re-implement the old coqdep on top of the new lexer.

As a bonus, this proposal has a non trivial performance benefit. We remove all the overhead of running additional binaries this way. It's something I've always wanted to experiment with ocamldep, but never got the time to :)

view this post on Zulip Enrico Tassi (Jun 11 2022 at 20:21):

Can you share pointers? I'm not even aware of the existence of Coqmod.

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 02:16):

Sure, this PR started the discussion https://github.com/coq/coq/pull/16153

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 05:21):

IIUC, this proposal doesn't seem to improve on this point from Emilio (https://github.com/coq/coq/pull/16153#issuecomment-1152370246), in fact it makes lexer updates harder since they're cross repo (IIUC?)

Having two tools that provide conflicting dependency information is not a good idea. It is indeed not related to coqmod per-se, but really about avoiding the situation where developers have to deal with two lexers when updating the language.

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 05:35):

I guess the point is letting coqmod stay experimental for a while, allowing it to break?

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 05:46):

new bugs in coqdep seem unlikely not reach users given Coq’s testsuite — but in your proposal you could iterate on coqmod much faster, IIUC

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 05:50):

If the above is correct, here are my actual 2 cents:
as a user, it seems safer if dune can keep using coqdep until coqmod stabilizes and is upstreamed, so that dune's coq support will not regress.

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 05:51):

Having the coqmod option sounds useful, as soon as it is stable enough and avoids the terrible coqdep performance in Coq 8.15

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 05:59):

meanwhile, does this affect the plans to speed up coqdep by running it once per-theory, as Emilio had proposed? If that were delayed, from a user’s POV, it might seem an instance of “the perfect is the enemy of the good”. Even with the improvement Emilio already did, this is still unfortunate.

view this post on Zulip Enrico Tassi (Jun 12 2022 at 07:31):

Thanks for the pointer. I think duplication of lexing code is minor compared to duplication of handling of -R and company. If coqmod does not resolve to files, then the logic must be duplicated in dune.
This is very worrying, the fact that rules for .v files are hardwired and not overrideable was a major pain when we changed the way cmxs are loaded: I wrote a crapload of compat code to unentangle the release of coq and dune.

view this post on Zulip Enrico Tassi (Jun 12 2022 at 07:34):

If the reason for developing coqmod is to speed things up, then the other path of calling coqdep once is way more reasonable to me.

view this post on Zulip Ali Caglayan (Jun 12 2022 at 11:25):

Let me be clear that coqmod will not know about -Q and -R, that is up to Dune to resolve (which it already does today). coqmod will simply report any statement that generates a dependency.

  1. If coqmod reports From X Require A, then Dune will need to do a resolution of X and then search for A.
  2. If coqmod reports Require A then Dune just needs to find A.
  3. If coqmod reports Decalre ML Module "foo" then Dune needs to search for an OCaml module.
  4. If coqmod reports Load "file.v", then Dune will search for this file. (this is if we keep wanting to support this in Coq).
  5. If coqmod reports From X Require Extra Dependency "asdf". we have to do something else.

coqmod will supply the first part, Dune will resolve the second.

Why do we want coqmod at all if coqdep does all of this for us?

The answer is that coqdep simply does too many things at once:

All of this work, if done per file, is mostly wasted work. Enrico suggests calling coqdep only once, this is possible but it comes at a cost. It does not scale well. If you have a large amount of .v files, coqdep will have to lex each and everyone of them to work out all the dependencies. So if you change a source file, you will have to do the lexing step again and again for everything.

What we can do is make the lexing step separate, this is what coqmod started off as. Now Dune can call coqmod incrementally for each .v file without having to lex the entire file system. coqmod will then report the statements I detailed above to Dune, and then Dune, which knows how to find files, will handle all the dependencies and flags passed to coqc/coqdoc/etc.

When separating the lexing step from coqdep, I noticed there are some poor properties. For instance, newlines were being eaten at random by the lexer, without reporting them to Lexing.lexbuf. This means that there was no good (ln/col) positional data for errors, only char count. Therefore I wrote the entire lexer from the beginning, carefully making sure that the locations work nicely.

Now as any programmer, I am somewhat confident in my own work, but I am not confident enough to shove my lexer into everybodys face by making coqdep use it. This is why I told Emilio that I do not want to share the lexer with coqdep... for the moment.

It appears natural to me for the time being, to take the coqmod tool upstream to Dune, where it can be more quickly iterated and improved together with thing it is designed for. Later, we can bring the polished result downstream to Coq, and if needed factor coqdep through coqmod.

Regarding why I chose a separate binary instead of just a coqdep -modules mode. This way, we wouldn't have to care about versioning. coqmod would also work with older versions of Coq. In fact, the more I think about it, the more sense it makes to completely split coqmod from the Coq release cycle.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:18):

I think you folks are turning something easy (sharing a lexer) into a much more complex and unrelated discussion.

Refactoring of logic for file resolution should also happen and be shared by Dune, but that's a separte concern.

If the coqmod lexer is not good to use by coqdep, how it is good to be used on its own then?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:23):

Ali Caglayan said:

Let me be clear that coqmod will not know about -Q and -R, that is up to Dune to resolve (which it already does today).

@Ali Caglayan , how does Dune resolves deps today? It does not, and as @Enrico Tassi has pointed out, that's significant tricky work.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:29):

It appears natural to me for the time being, to take the coqmod tool upstream to Dune, where it can be more quickly iterated and improved together with thing it is designed for. Later, we can bring the polished result downstream to Coq, and if needed factor coqdep through coqmod.

Regarding why I chose a separate binary instead of just a coqdep -modules mode. This way, we wouldn't have to care about versioning. coqmod would also work with older versions of Coq. In fact, the more I think about it, the more sense it makes to completely split coqmod from the Coq release cycle.

I can see why it appears natural you, but I also think that you don't have the full picture of the amount of work needed for this to happen, as you have just assumed that Dune is able to do Coq's loadpath resolution, but unfortunately, it is not, and the amount of code that is used in Coq to implement that is of the size of the full Coq Dune implementation.

So indeed, the strategy of keeping specific-knowledge about Coq's vernacular in Dune is a very risky one, as the moment Coq updates its vernacular Dune is S.O.L. Moreover, the work/benefit ratio of coqmod is as of today, very very high. That's a lot of work for very little benefit. There are, in my opinion, way more important things.

I think the right way to go about this, is for Coq to maintain the parts specific to Coq's vernacular as libraries, and for Dune to vendor them.

Moreover, this is also something doc managers and tools with more advanced package management such as jsCoq do need too. So your approach would imply a large duplication of logic and code that can't go very well for anybody involved.

view this post on Zulip Ali Caglayan (Jun 12 2022 at 12:41):

Emilio Jesús Gallego Arias said:

Ali Caglayan said:

Let me be clear that coqmod will not know about -Q and -R, that is up to Dune to resolve (which it already does today).

Ali Caglayan , how does Dune resolves deps today? It does not, and as Enrico Tassi has pointed out, that's significant tricky work.

Dune today, is able to map logical names to directories. It just needs to pass these as -Q parameters to coqc which will be doing the actual loading

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:42):

All of this work, if done per file, is mostly wasted work. Enrico suggests calling coqdep only once, this is possible but it comes at a cost. It does not scale well. If you have a large amount of .v files, coqdep will have to lex each and everyone of them to work out all the dependencies. So if you change a source file, you will have to do the lexing step again and again for everything.

That reasoning is a bit strange, in the sense that yes, maybe the work done per file is wasted, but you are just moving where the work will be done. Putting this in Dune won't reduce the amount of work to be done at all, you will just indeed share the scanning of the FS.

Moreover, all this work takes a trivial amount of time. Lexing + resolution is on the microseconds with modern processors. So you are gaining a very little time in the build.

For me, separation is useful not for performance (which I'm willing to be is just a very marginal improvement, in the order of 200 microseconds per file) but in that it allows you to support more advanced features; like in jsCoq, we have a hack now to download libraries lazily from the web when a Require happens. A much more interesting use cases.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:43):

But for that we need coqmod and also more stuff for loadpath handling. In fact, it is even possible that once we implement the required infrastructure for Coq and Flèche, coqmod is just redundant, as things work in a say similar to what DAP could be.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:44):

Dune today, is able to map logical names to directories. It just needs to pass these as -Q parameters to coqc which will be doing the actual loading

Yes, that's trivial. What is not trivial (and Dune can't do yet) is to map From Foo Require A to a file.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:46):

It makes sense to move this mapping to Dune indeed, but should happen by vendoring Coq's coq-core.loadpath library.

view this post on Zulip Ali Caglayan (Jun 12 2022 at 12:46):

So indeed, the strategy of keeping specific-knowledge about Coq's vernacular in Dune is a very risky one, as the moment Coq updates its vernacular Dune is S.O.L. Moreover, the work/benefit ratio of coqmod is as of today, very very high. That's a lot of work for very little benefit. There are, in my opinion, way more important things.

The benefit is this. We can develop coqmod in tandem with Dune, get it working well. Allow for some reassurance that coqdep and coqmod are doing the same thing, which allows us to move coqmod back into Coq and refactor coqdep. There are still implementation details needing to be sorted out on the Dune side.

Maybe I didn't stress this enough, but coqmod would not be replacing coqdep on the Dune side. Dune will still work with coqdep for the time being, I am just suggesting a way we can develop these tools further.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:47):

Ali Caglayan said:

So indeed, the strategy of keeping specific-knowledge about Coq's vernacular in Dune is a very risky one, as the moment Coq updates its vernacular Dune is S.O.L. Moreover, the work/benefit ratio of coqmod is as of today, very very high. That's a lot of work for very little benefit. There are, in my opinion, way more important things.

The benefit is this. We can develop coqmod in tandem with Dune, get it working well. Allow for some reassurance that coqdep and coqmod are doing the same thing, which allows us to move coqmod back into Coq and refactor coqdep. There are still implementation details needing to be sorted out on the Dune side.

Maybe I didn't stress this enough, but coqmod would not be replacing coqdep on the Dune side. Dune will still work with coqdep for the time being, I am just suggesting a way we can develop these tools further.

How is this a benefit? It seems more work to me

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:49):

You can of course have a dev branch where you have coqmod vendored for quick development, you need to vendor loadpath.ml too

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:50):

but in the end, you wanna this to live in the Coq repos, so when coq devs change the vernacular they update coqmod

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:50):

To be clear, it is more work the moment you put that code in a released dune version

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:50):

then you are S.O.L.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:51):

for developing of course you do the way is best for your own dev workflow

view this post on Zulip Ali Caglayan (Jun 12 2022 at 12:51):

There is something I don't quite understand here. You say that loadpath resolution needs to be duplicated in Dune. Why? When I write From A Require B. I imagine that Dune will be able to look for a coq.theory called A perhaps a partial match like mathcomp or a more specific one like Coq.Arithmetic. Then it would have to search in the scope of that theory for a file called A. The rules for which are not that complicated, and Dune can already detect ambiguous paths.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:52):

If you don't duplicate it, how are you gonna map the From A Require B to an actual file.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:52):

Complicated is indeed a subjective measure

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:52):

indeed, in the grand scheme of Coq or Dune codebase they are certainly pretty trivial

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:52):

but they have a lot of cases to handle

view this post on Zulip Ali Caglayan (Jun 12 2022 at 12:52):

In Coq this is a lot of work because there is no (usable) existing infrastructure for crawling for dependencies. Dune already has such a thing.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:52):

due to overlaps and ambiguity, the code is the you can check it

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:53):

Ali Caglayan said:

In Coq this is a lot of work because there is no (usable) existing infrastructure for crawling for dependencies. Dune already has such a thing.

What is exactly the part of current Coq codebase that is complex but Dune's API would replace?

view this post on Zulip Ali Caglayan (Jun 12 2022 at 12:53):

In coqdep, there is code to crawl entire directories recursively, and check for duplicate/ambiguous files.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:53):

What is the Dune infrastructure you are referring too? I'm not aware of it

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:54):

Yes, that code is duplicated in coqdep and coqc

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:54):

but that code is very Coq specific, I'm not sure Dune has code to do this

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:54):

first step is to get rid of the duplication

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:54):

also coqdoc has this code a bit

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:55):

crawling the directories is the easy part, the hard part is to build the map

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:55):

well, not hard, but subtle

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:55):

as there is a lot of cases to handle

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:55):

would be great to actually reduce what's allowed

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:55):

that can go in parallel with the rest of the work

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:56):

but actually that's a good example of the dangers of duplicating logic

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:56):

Coq developers may choose to fix some of the bad semantics of -Q

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:56):

so actually less behaviors are allowed

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:56):

now, that happens in Coq master, and now, unless you vendor that code, you have a lot of work to understand Coq's change, port it to Dune, and test it properly

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:57):

and moreover, you have no real guarantees that code is doing the same

view this post on Zulip Ali Caglayan (Jun 12 2022 at 12:58):

Emilio Jesús Gallego Arias said:

Coq developers may choose to fix some of the bad semantics of -Q

Do you have a concrete example of this, or is it just a hyppothetical?

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 12:58):

Paolo Giarrusso said:

If the above is correct, here are my actual 2 cents:
as a user, it seems safer if dune can keep using coqdep until coqmod stabilizes and is upstreamed, so that dune's coq support will not regress.

The problem is that dune cannot progress with improving support in many ways without coqmod.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 12:59):

Rudi Grinberg said:

Paolo Giarrusso said:

If the above is correct, here are my actual 2 cents:
as a user, it seems safer if dune can keep using coqdep until coqmod stabilizes and is upstreamed, so that dune's coq support will not regress.

The problem is that dune cannot progress with improving support in many ways without coqmod.

Then add coqmod to Coq, and vendor it for previous versions, but you need to be careful indeed as the syntax of Coq has changed

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 12:59):

Enrico Tassi said:

Thanks for the pointer. I think duplication of lexing code is minor compared to duplication of handling of -R and company. If coqmod does not resolve to files, then the logic must be duplicated in dune.
This is very worrying, the fact that rules for .v files are hardwired and not overrideable was a major pain when we changed the way cmxs are loaded: I wrote a crapload of compat code to unentangle the release of coq and dune.

I don't know why this was difficult, but did you look into the changing the coq rules in dune at all? If so, what was difficult about it?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:00):

Ali Caglayan said:

Emilio Jesús Gallego Arias said:

Coq developers may choose to fix some of the bad semantics of -Q

Do you have a concrete example of this, or is it just a hyppothetical?

I have a concrete example, like we just did forbidding certain kind of ambigous paths, and we'd like to forbid more.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:00):

There are several issues opened about it

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:00):

Enrico Tassi said:

If the reason for developing coqmod is to speed things up, then the other path of calling coqdep once is way more reasonable to me.

That yields poor incremental performance. It's how it used to work for ocamldep but we changed it for this reason.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:02):

Rudi Grinberg said:

Enrico Tassi said:

Thanks for the pointer. I think duplication of lexing code is minor compared to duplication of handling of -R and company. If coqmod does not resolve to files, then the logic must be duplicated in dune.
This is very worrying, the fact that rules for .v files are hardwired and not overrideable was a major pain when we changed the way cmxs are loaded: I wrote a crapload of compat code to unentangle the release of coq and dune.

I don't know why this was difficult, but did you look into the changing the coq rules in dune at all? If so, what was difficult about it?

Actually the amount of code to support the old loading model is very little. It is more that was hard to figure out how to do it.

The main difficulty we have to fix Dune rules is a) lack of manpower and will b) bugs in Dune such as https://github.com/ocaml/dune/issues/5833

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:02):

Emilio Jesús Gallego Arias said:

Ali Caglayan said:

Emilio Jesús Gallego Arias said:

Coq developers may choose to fix some of the bad semantics of -Q

Do you have a concrete example of this, or is it just a hyppothetical?

I have a concrete example, like we just did forbidding certain kind of ambigous paths, and we'd like to forbid more.

I still don't understand, what more do you want to forbid?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:02):

Rudi Grinberg said:

Enrico Tassi said:

If the reason for developing coqmod is to speed things up, then the other path of calling coqdep once is way more reasonable to me.

That yields poor incremental performance. It's how it used to work for ocamldep but we changed it for this reason.

The proportional cost is very little in Coq, due to the different compilation ratio time.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:03):

Ali Caglayan said:

Emilio Jesús Gallego Arias said:

Ali Caglayan said:

Emilio Jesús Gallego Arias said:

Coq developers may choose to fix some of the bad semantics of -Q

Do you have a concrete example of this, or is it just a hyppothetical?

I have a concrete example, like we just did forbidding certain kind of ambigous paths, and we'd like to forbid more.

I still don't understand, what more do you want to forbid?

See the issues opened, but for sure I want to to keep evolving the current semantics.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:04):

So yes, coqmod is nice to have, but the actual benefit for the users will be minimal

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:04):

Don't put a sad face, my time is limited Ali :(

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:04):

There is just so much I can do

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:05):

That reasoning is a bit strange, in the sense that yes, maybe the work done per file is wasted, but you are just moving where the work will be done. Putting this in Dune won't reduce the amount of work to be done at all, you will just indeed share the scanning of the FS.

Moreover, all this work takes a trivial amount of time. Lexing + resolution is on the microseconds with modern processors. So you are gaining a very little time in the build.

Every single change will require the batch job to re-read every single file in the theory. The amount of work is proportional to the amount of files in the theory. Every single file needs to be scanned before any actual useful compilation work is started.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:05):

So I will indeed just summarize: duplication of Coq-specific logic makes little sense and will create a large maintenance pain. We should have a single source of truth w.r.t. how Coq loading semantics work, and have tools vendor it.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:05):

Rudi Grinberg said:

That reasoning is a bit strange, in the sense that yes, maybe the work done per file is wasted, but you are just moving where the work will be done. Putting this in Dune won't reduce the amount of work to be done at all, you will just indeed share the scanning of the FS.

Moreover, all this work takes a trivial amount of time. Lexing + resolution is on the microseconds with modern processors. So you are gaining a very little time in the build.

Every single change will require the batch job to re-read every single file in the theory. The amount of work is proportional to the amount of files in the theory. Every single file needs to be scanned before any actual useful compilation work is started.

Yes, this takes _microseconds_

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:06):

In OCaml you feel it more, as compilation is much faster

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:06):

so that's a nice thing to have, just users won't see a lot of benefit

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:06):

cutting couple of seconds of a 30 mins build

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:07):

Already the time I spent writing here, I would have ported coqdep to use the new lexer

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:07):

because, if the new lexer is not good for coqdep, there is no way is good for anything else

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:07):

as it has to be buggy then

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:08):

Yes, of course it's meaningless for a clean build. It is however quite useful for tiny changes that you'd expect instant feedback for. I highly doubt it's going to be microseconds in the first place, but even if it is, it's microseconds before dune will start the coqc jobs. So the delay is microseconds * the number of cores.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:08):

There are virtually no cases when you can get instant feedback from .v -> .vo compilation

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:09):

just the loading of deps makes coqdep take several seconds

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:09):

due to marshall

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:09):

Emilio Jesús Gallego Arias said:

There are virtually no cases when you can get instant feedback from .v -> .vo compilation

There are with the cache :)

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:09):

Emilio Jesús Gallego Arias said:

Don't put a sad face, my time is limited Ali :(

This is not a sad face but a confused one. I still don't get what you want to change about -Q.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:09):

now you are talking about a document server, but that's beyond what dune can do today, for intra-file changes

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:10):

Emilio Jesús Gallego Arias said:

now you are talking about a document server, but that's beyond what dune can do today, for intra-file changes

Who is talking about a document server?!

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:10):

Emilio Jesús Gallego Arias said:

because, if the new lexer is not good for coqdep, there is no way is good for anything else

I suppose we both are concerned about this, but are addressing it differently:

  1. you'd like to modify to coqdep to determine this
  2. I'd like to build coq-universe to do so instead

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:10):

Rudi Grinberg said:

Emilio Jesús Gallego Arias said:

There are virtually no cases when you can get instant feedback from .v -> .vo compilation

There are with the cache :)

Ok, but even so, people rarely use this workflow in Coq, they never call coqc on files they are working on, they use interfactive mode.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:11):

so actually vendoring loadpath makes even more sense, because you need Coq support to improve the common interactive workflow

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:11):

and in this case you don't even need coqmod

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:11):

Coq can callback on Dune when Require is found

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:12):

Anyways I like coqdep

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:12):

coqmod sorry

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:12):

Ali Caglayan said:

Emilio Jesús Gallego Arias said:

Don't put a sad face, my time is limited Ali :(

This is not a sad face but a confused one. I still don't get what you want to change about -Q.

Specifically, we are not asking you to implement any changes in Coq, but why you are against this one in the first place?

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:12):

So we went from re-implementing coqdep on top of coqmod to throwing coqmod away? :thinking:

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:12):

and while it is not gonna make a large impact compared to other features, of course I'd be amazing to have it and many people would be very happy with this improvement

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:12):

nobody is questioning that

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:12):

what I'm questioning is that having 2 lexers is a very bad idea

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:13):

Is it not just a temporary state though?

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:13):

Emilio Jesús Gallego Arias said:

what I'm questioning is that having 2 lexers is a very bad idea

Give me some time, let me write a reply to this.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:13):

Temporary is fine, but porting takes a few mins

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:13):

actually I didn't port it myself as then I can't merge the PR

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:14):

and in fact, the CI would be a good test for the new lexer

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:14):

Emilio Jesús Gallego Arias said:

Temporary is fine, but porting takes a few mins

Please don't do this!

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:14):

Why do you care?

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:14):

You will be forcing possibly buggy code on the rest of the Coq users

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:14):

that's touching coqdep, not coqmod

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:14):

then if the code is buggy, it should be fixed ASAP right?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:14):

why you want to work with buggy code then?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:15):

Then you'll have to debug Coq universe, that won't be fun

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:15):

No code in production starts of bug free. It goes through cycles of testing and then deployment.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:15):

Yes, that's why we have a CI

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:15):

and 2.5k bugs open

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:15):

The CI has ok coverage but it won't cover every case.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:15):

it won't eys

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:15):

it won't yes

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:15):

So why needlessly put users through this?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:15):

but that's our current method to determine "it works"

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:16):

If we can factor coqdep in the future through coqmod once it has been tested further?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:16):

Ali Caglayan said:

So why needlessly put users through this?

I thought the idea was for users to use coqmod in the end?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:16):

Well, a good way to start testing is to use the lexer in Coq's CI

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:16):

Right, but I need to turn an experiment into a solution in the meantime.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:16):

Right, and how do you plan to test it then?

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:17):

You know, even if you implement coqdep on top of coqmod (Something that I think is a good idea - at least eventually), it would still be far simpler to iterate with coqmod + dune if coqmod is vendored in dune.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:17):

Rudi Grinberg said:

You know, even if you implement coqdep on top of coqmod (Something that I think is a good idea - at least eventually), it would still be far simpler to iterate with coqmod + dune if coqmod is vendored in dune.

The lexer of .v files is all you care

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:17):

I don't see what you gain of forking that in Dune

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:17):

the grammar itself I mean

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:17):

We are not forking any grammar?

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:18):

The lexer is only 200 lines

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:18):

Yes, as I said porting coqdep to use the new lexer would have taken 5 mins

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:18):

and if you have bugs, you can start fixing them

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:18):

Emilio Jesús Gallego Arias said:

I don't see what you gain of forking that in Dune

Well it's a tiny component that allows us to unlock some deeper changes in dune. Once we're satisfied with the results on the dune side, we can know for sure that coqmod is good enough to be upstreamed.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:19):

and it is great you wrote a new lexer, the old one was very very old and needed a modern rewrite, so I'm looking forward to replace the old lexer

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:19):

Rudi Grinberg said:

Emilio Jesús Gallego Arias said:

I don't see what you gain of forking that in Dune

Well it's a tiny component that allows us to unlock some deeper changes in dune. Once we're satisfied with the results on the dune side, we can know for sure that coqmod is good enough to be upstreamed.

The criteria for coqmod's lexer to be upstreamed is to work with Coq's CI

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:19):

that's the main criteria

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:19):

so seems wise to start with that step

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:19):

Right, but this is future work. Which doesn't make sense to do at the moment.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:19):

and be sure you have a lexer that works

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:20):

because otherwise you are gonna find youself debugging very weird build errors

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:20):

And if you don't want experimental tools in Coq, fine.

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:20):

We can develop in dune and usptream later.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:20):

Not in released code in Dune either

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:20):

so of course I'm talking about released code

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:20):

At no point did I say I would replace Dune's coq support with coqmod?

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:21):

It is an experiment that we would like to conduct.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:21):

I don't know, I was not talking about Dune, but about https://github.com/coq/coq/pull/16153

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:21):

and what needs for it to be merged

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:21):

Right, I will close that and develop coqmod in Dune.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:21):

Will you put coqmod in Dune's main branch?

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:21):

So that in the future I am happy for it to be factored with coqdep

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:22):

So you are gonna do your own ad-hoc testing instead of profiting from Coq's infrastructure?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:22):

Seems like a bad plan to me

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:22):

How are you gonna determine you are happy with the lexer?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:23):

Because as of today, the only way we have to measure "the lexer works" is Coq's CI

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:23):

IIANM

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:23):

Emilio you've said before the lexer is a trivial amount of work. Why are we dwelling on it? Let's do it once the whole feature is ready. Why block a massive chunk of work on some tiny change that will not impact anyone in the short/medium term? Even if the lexer is bad, we'll have 1000 opportunities to fix it before releasing anything.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:23):

Porting coqdep to the new lexer is a trivial amount of work

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:23):

The whole lexer thing is a distraction, we should have just used coqdep's lexer to avoid this whole issue.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:23):

and gives you very valuable testing

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:24):

so what's the argument against it?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:24):

Rudi Grinberg said:

The whole lexer thing is a distraction, we should have just used coqdep's lexer to avoid this whole issue.

Yes I agree, tho the new lexer is very nice

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:24):

Don't fix what's not broken?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:24):

So I'd love to see it upstreamed

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:24):

Rudi Grinberg said:

Emilio you've said before the lexer is a trivial amount of work. Why are we dwelling on it? Let's do it once the whole feature is ready. Why block a massive chunk of work on some tiny change that will not impact anyone in the short/medium term? Even if the lexer is bad, we'll have 1000 opportunities to fix it before releasing anything.

I'm dwelling on it because there is this PR I want to get merged!

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:25):

If we put this in Coq, factored through coqdep today, it will be impossible to make any changes for Dune.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:25):

Ali Caglayan said:

Don't fix what's not broken?

Well the old lexer seems to be broken , for example it didn't report positions etc... it was not exactly broken, but needing a rewrite, and I like a lot the new one

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:26):

Ali Caglayan said:

If we put this in Coq, factored through coqdep today, it will be impossible to make any changes for Dune.

Put just the new lexer if you want

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:26):

that's OK for me

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:26):

but actually coqmod has nothing else

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:26):

than the lexer

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:26):

why would you need to change the lexer for Dune?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:26):

you may have, but you can submit a PR to Coq

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:26):

This is slow

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:27):

Well, then keep your copy, fine

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:27):

but that copy can't be exposed to users

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:27):

Emilio Jesús Gallego Arias said:

so what's the argument against it?

I'm not arguing against it. I just have no opportunity to compel anyone to work on what I want. When I fail to do so, I just try to make progress from another angle :)

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:28):

Emilio Jesús Gallego Arias said:

but that copy can't be exposed to users

The only reason being is that you wanted to factor through coqdep when it wasn't ready.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:28):

The thing is, a new lexer was written. I like it a lot. However, if that lexer is gonna be used by final users, I don't care if in Dune or Coq, it has to be properly tested.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:28):

Ali Caglayan said:

Emilio Jesús Gallego Arias said:

but that copy can't be exposed to users

The only reason being is that you wanted to factor through coqdep when it wasn't ready.

Well, everything looked ready to me in the PR, except for getting rid of the old lexer

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:29):

Let's get rid of it in a future PR

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:29):

That way we can test it there too.

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:29):

How about we just leave the PR open for now until we have something working in dune? What's the rush to merge it?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:29):

Ali Caglayan said:

Let's get rid of it in a future PR

I'm afraid I can't support having two lexers in the codebase, even if that's temporary.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:30):

Rudi Grinberg said:

How about we just leave the PR open for now until we have something working in dune? What's the rush to merge it?

Not a rush, but I bet is ready.

I think indeed it is very important to test the lexer before you make progerss on the Dune side, makes little sense to me that you start using in Dune a new untested lexer that could create you a lot of unrealted trouble.

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:30):

As of today, coqmod is potentially only useful as an implementation detail of dune's rules.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:31):

@Rudi Grinberg if we listen to what Ali is suggesting, coqmod could give you wrong dep analysis too

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:31):

Coqmod does no dep analysis!

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:31):

It just reports tokens that introduce deps

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:31):

Emilio Jesús Gallego Arias said:

Rudi Grinberg said:

How about we just leave the PR open for now until we have something working in dune? What's the rush to merge it?

Not a rush, but I bet is ready.

I think indeed it is very important to test the lexer before you make progerss on the Dune side, makes little sense to me that you start using in Dune a new untested lexer that could create you a lot of unrealted trouble.

It will not cause us trouble because it will take us a while to modify things enough to even use it correctly. Once we get to the point where we can actually run things, we'll consider these questions.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:31):

how is that different from dep analysis?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:32):

Rudi Grinberg said:

Emilio Jesús Gallego Arias said:

Rudi Grinberg said:

How about we just leave the PR open for now until we have something working in dune? What's the rush to merge it?

Not a rush, but I bet is ready.

I think indeed it is very important to test the lexer before you make progerss on the Dune side, makes little sense to me that you start using in Dune a new untested lexer that could create you a lot of unrealted trouble.

It will not cause us trouble because it will take us a while to modify things enough to even use it correctly. Once we get to the point where we can actually run things, we'll consider these questions.

Indeed, and that's the second problem, to do so, you will have to duplicate a logic that is already inconsistent in Coq's own codebase, introducing a 4th version of the resolution rules.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:32):

So we all would be better off with continuing the work on coq-core.loadpath and having Dune vendor it.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:33):

I am positive we will change resolution rules, for (using coq 2.0) for example

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:33):

so we want an easy way to keep coqc and dune in sync

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:33):

so it is very easy, we are just making things complex

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:34):

Tho I insist again that I'm talking about the point things get upstreamed to Coq or Dune

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:34):

of course you can experiment a lot

view this post on Zulip Gaëtan Gilbert (Jun 12 2022 at 13:34):

Emilio Jesús Gallego Arias said:

Ali Caglayan said:

Let's get rid of it in a future PR

I'm afraid I can't support having two lexers in the codebase, even if that's temporary.

I very agree

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:34):

but again Ali you didn't answer to what is the concrete problem in having Coq's CI using coqmod's new lexer

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:34):

it takes you 5 minutes

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:34):

and you get a lot of feedback on your lexer

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:35):

if it works, we can push it

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:35):

if it doesn't, you already know you have problem

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:35):

you may choose to ignore it

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:35):

but you know that when using your Dune coqmod branch in Coq Universe

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:35):

you'll be in problems

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 13:35):

@Emilio Jesús Gallego Arias you seem to be claiming there are no downsides in the slower development cycle, and that's too strong —

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 13:36):

all the downsides you point out are real, of course

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:36):

@Paolo Giarrusso , more concretely, I claim that in the list of TODOs I have in Dune, cutting two seconds of a build seems low to me

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:36):

for example, it is much more prioritary to have better doc build, and to allow people to do opam packages with Dune

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:37):

and make dune-release work

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 13:37):

I also agree that incremental lexing is a distraction

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:37):

coqmod is great

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:37):

the discussion gets sidetracked all the time

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:38):

because as a Coq dev I'm only interested in upstreaming a new lexer

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:38):

Emilio Jesús Gallego Arias said:

So we all would be better off with continuing the work on coq-core.loadpath and having Dune vendor it.

I disagree that "our" efforts are better off spent working on one whatever you think is the highest priority. That is not how progress is made in the open source world. It's in fact how contributors get discouraged and abandon projects.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:38):

which is a great thing as we really needed to replace the old one

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:38):

Rudi Grinberg said:

Emilio Jesús Gallego Arias said:

So we all would be better off with continuing the work on coq-core.loadpath and having Dune vendor it.

I disagree that "our" efforts are better off spent working on one whatever you think is the highest priority. That is not how progress is made in the open source world. It's in fact how contributors get discouraged and abandon projects.

Fair point, tho my thinking is backed by my quantitative / qualitative analysis

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 13:39):

@Emilio Jesús Gallego Arias nobody has conclusive quantitative analysis of software development costs :-)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:39):

So I'm open to reconsider my plan, but I'm asking about the advantages of the alterantive plan, what are they?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:39):

In the open source world, we many times do plans that go really bad!

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:40):

My analysis is not conclusive, it is just my analysis, which I'm willing to reconsider

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:40):

note how many questions I've asked and quite a few got no answer

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:40):

Paolo Giarrusso said:

Emilio Jesús Gallego Arias nobody has conclusive quantitative analysis of software development costs :-)

I've indeed updated my sentenced to highlight that this is, of course, my analysis!

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:41):

In Coq for example, someone thought that having 3 different implementations of loadpath resolution was a good idea

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:41):

blocking a massive branch of work on "5 minutes of work" does not sound quantitatively sound to me. I'm sympathetic to the correctness concerns, but honestly it's not enough to spook me off. There's a dozen of other issues that we'll be able to solve once we have coqmod in dune that are completely unrelated and will benefit everyone no matter what lexer is used.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:42):

Rudi Grinberg said:

blocking a massive branch of work on "5 minutes of work" does not sound quantitatively sound to me. I'm sympathetic to the correctness concerns, but honestly it's not enough to spook me off. There's a dozen of other issues that we'll be able to solve once we have coqmod in dune that are completely unrelated and will benefit everyone no matter what lexer is used.

how's the branch blocked @Rudi Grinberg ?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:42):

who's blocking anything? (and how?)

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 13:42):

@Emilio Jesús Gallego Arias the point is that there are _sometimes_ advantages to starting over and prototyping from scratch

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:43):

Of course @Paolo Giarrusso , I do all the time myself, just go and see my projects on github

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:43):

I have reimplemented quite a few components from scratch just for Coq

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 13:43):

good we agree here

view this post on Zulip Gaëtan Gilbert (Jun 12 2022 at 13:43):

Emilio Jesús Gallego Arias said:

In Coq for example, someone thought that having 3 different implementations of loadpath resolution was a good idea

coqc/coqdep/??? what's the 3rd?

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:43):

Nor do I suggest forking anything. I'd be interested in fixing the loadpath issues as well if I understood them better. I'm just mentally prepared to work on the coqmod stuff already and have a good idea of how to go about it. Once I get to that state with loadpath, I'd be interested in adapting dune to use that.

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 13:43):

hope we also agree that the prototypes will not be feature-complete/pass 100% tests/etc etc early on

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:44):

Gaëtan Gilbert said:

Emilio Jesús Gallego Arias said:

In Coq for example, someone thought that having 3 different implementations of loadpath resolution was a good idea

coqc/coqdep/??? what's the 3rd?

coqchk and coqdoc :S

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:44):

haha so I forgot how to count

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:44):

let's get rid of that stuff Gaëtan

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:45):

Well coqchk and coqdoc make half each, so it is 1 + 1 + 0.5 + 0.5 = 3

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 13:45):

I can't really imagine why you'd need much prototyping in _the lexer_ (or parser, I'd say), but I can imagine the _API_ might need iteration; much more likely, the loadpath API might need iteration

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:45):

So what do you want to do Emilio? I guess I can hack coqdep to use the new lexer, would that be sufficient?

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:45):

Emilio Jesús Gallego Arias said:

who's blocking anything? (and how?)

Great, so how about this: let's get coqmod working in dune. Put it behind an experimental flag. Then re-asses once we determine if it's actually a useful thing.

view this post on Zulip Gaëtan Gilbert (Jun 12 2022 at 13:45):

coqchk and coqdoc at least get to work with only absolute paths (not sure about coqdoc)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:46):

@Paolo Giarrusso it needs a lot of iteration, but actually you need to update Coq itself. So for jsCoq I can afford to fork Coq, but for example, for SerAPI I need to push upstream. That's indeed very slow and frustrating :(

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:46):

Ali Caglayan said:

So what do you want to do Emilio? I guess I can hack coqdep to use the new lexer, would that be sufficient?

Sufficient for what?

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 13:47):

we seem to all agree that eventually, you need to update Coq, but for the prototype you might not want to.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:47):

Gaëtan Gilbert said:

coqchk and coqdoc at least get to work with only absolute paths (not sure about coqdoc)

That's why I counted them like less than one , so indeed maybe we can write them off, but there is at least the command line parsing logic etc...

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:47):

also coqlib detection

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:48):

Emilio Jesús Gallego Arias said:

Gaëtan Gilbert said:

Emilio Jesús Gallego Arias said:

In Coq for example, someone thought that having 3 different implementations of loadpath resolution was a good idea

coqc/coqdep/??? what's the 3rd?

coqchk and coqdoc :S

Perhaps what is missing here is a standard rather than a single implementation. The fact that there's 3 different wrappers around walking the file system is not what's scaring me. It's that nobody knows when is one of them is incorrect.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:48):

Rudi Grinberg said:

Emilio Jesús Gallego Arias said:

who's blocking anything? (and how?)

Great, so how about this: let's get coqmod working in dune. Put it behind an experimental flag. Then re-asses once we determine if it's actually a useful thing.

Sure that sound good, and it is for sure useful.

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 13:48):

okay, that sounds like progress SwEng side!

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:53):

Emilio Jesús Gallego Arias said:

Ali Caglayan said:

So what do you want to do Emilio? I guess I can hack coqdep to use the new lexer, would that be sufficient?

Sufficient for what?

Ping @Ali Caglayan (gonna head to cook lunch in a minute)

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:53):

I meant for making progress, but it looks like we agree on "vendoring" in Dune now?

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:54):

upstreaming is a strong work. just getting it working in the simplest way possible is the goal.

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:54):

then we argue about what lives where

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:54):

@Ali Caglayan what does upstreaming to Dune mean?

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:54):

I can keep the PR open, and when we deem coqmod ready for general use, we can add it to the Coq repo with the coqdep changes too.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:54):

(I bet there are more)

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:55):

By the way, I've moved the discussion into two disucssions

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:55):

This is now about coqmod

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:55):

The other is about loadpath resolution

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:55):

Ali Caglayan said:

I can keep the PR open, and when we deem coqmod ready for general use, we can add it to the Coq repo with the coqdep changes too.

That sounds good, at your will, I think the PR is ready to merge tho, I'd be surprised the lexer is buggy (and if it is buggy IMHO you want to learng about it sooner than later)

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:56):

@Emilio Jesús Gallego Arias did you make sure that coqmod doesn't introduce any loadpath related inconsistencies? at least from the test suite?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:56):

But before I go let's make sure we are on the same page on what "upstreaming to Dune" means

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:57):

We add coqmod into dune, it doesn't need any code from the Coq library anyway.

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:57):

Emilio Jesús Gallego Arias said:

But before I go let's make sure we are on the same page on what "upstreaming to Dune" means

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:58):

Ok, that sounds good, tho I still don't understand why you want to do the first item

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:59):

Because package managers suck. Opam especially so

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:59):

What I would do is to put coqmod in Coq and then vendor it

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:59):

but it is up to you

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 14:00):

Tbh, it would have allowed us to move even faster if we did it this way from the start. All that discussion about serialization could have been avoided completely.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:00):

or at least the lexer part

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:00):

Rudi Grinberg said:

Tbh, it would have allowed us to move even faster if we did it this way from the start. All that discussion about serialization could have been avoided completely.

that would depend on how buggy the new lexer is. If the lexer is buggy, I bet you save time by testing it in Coq's CI first

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 14:00):

Emilio Jesús Gallego Arias said:

or at least the lexer part

@Ali Caglayan If you can work on upstreaming the lexer in coqdep, that would be nice.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:00):

anyways I think the point is clear

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 14:01):

Emilio Jesús Gallego Arias said:

Rudi Grinberg said:

Tbh, it would have allowed us to move even faster if we did it this way from the start. All that discussion about serialization could have been avoided completely.

that would depend on how buggy the new lexer is. If the lexer is buggy, I bet you save time by testing it in Coq's CI first

I agree. Once we're at the point where testing can even be considered, let's think about verifying correctness ASAP.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:04):

You can test now if you want

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:06):

That was my whole point

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:11):

Right, but we don't have the Dune side implementation yet :))

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:11):

That needs to be done first.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:13):

I meant the lexer

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:13):

Indeed we would have saved more than 1h discussion if we had just pushed the 5 mins change

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:14):

I don't think it is 5min work as you claim, but I can submit a commit showing coqdep factored thru

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:14):

coqmod relies on csexp as a private lib

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:14):

so I can't make a coqmod lib

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:15):

I need to pull all the csexp stuff away

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:15):

thats more than 5 min work unfortunately.

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:15):

But I guess mostly my fault for intertwining it this way.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:19):

I offered to do that too

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:19):

you just need to pull the lexer

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:19):

then you flatten, and iterate

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:28):

@Emilio Jesús Gallego Arias Do you want to do it?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:30):

As you prefer!

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:30):

If that's boring for you I can push

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 15:22):

I did port it, see PR

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 15:23):

however there are many parsing problems I'm afraid

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 15:23):

Can't even parse most of Coq's stdlib

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 15:23):

Seems to require significant work


Last updated: Jan 30 2023 at 17:03 UTC