Coqdep vs. Coqmod · Dune devs & users

Stream: Dune devs & users

Topic: Coqdep vs. Coqmod

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:

If coq includes two dependency analysis tools that diverge, it doesn't look good. Especially if one tool is only usable with unreleased versions of some build system that is subject to change.
The corollary to that is that we might introduce bugs to coqdep by refactoring it to share as much code as possible. That's hard to justify to users as well. The way they will see it is that we just broke people's workflows without good reason.
The new coqmod tool is still experimental and is subject to change to accommodate dune's whims. On the other hand, modifying it will require more work if we need to make sure coqdep isn't broken.

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 :)

Enrico Tassi (Jun 11 2022 at 20:21):

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

Rudi Grinberg (Jun 12 2022 at 02:16):

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

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.

Paolo Giarrusso (Jun 12 2022 at 05:35):

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

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

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.

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

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. EDIT: this is OT here, I posted on the other thread

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.

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.

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.

If coqmod reports From X Require A, then Dune will need to do a resolution of X and then search for A.
If coqmod reports Require A then Dune just needs to find A.
If coqmod reports Decalre ML Module "foo" then Dune needs to search for an OCaml module.
If coqmod reports Load "file.v", then Dune will search for this file. (this is if we keep wanting to support this in Coq).
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:

It lexes a file, searches for .v files in the source tree, lexes them also.
Scans the entire of user-contrib for files.
Has various plugin finding helpers.

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.

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?

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.

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.

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

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.

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.

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.

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.

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.

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

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

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

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 12:50):

then you are S.O.L.

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

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.

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.

Emilio Jesús Gallego Arias (Jun 12 2022 at 12:52):

Complicated is indeed a subjective measure

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 12:52):

but they have a lot of cases to handle

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.

Emilio Jesús Gallego Arias (Jun 12 2022 at 12:52):

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

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?

Ali Caglayan (Jun 12 2022 at 12:53):

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

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 12:54):

Yes, that code is duplicated in coqdep and coqc

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 12:54):

first step is to get rid of the duplication

Emilio Jesús Gallego Arias (Jun 12 2022 at 12:54):

also coqdoc has this code a bit

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 12:55):

well, not hard, but subtle

Emilio Jesús Gallego Arias (Jun 12 2022 at 12:55):

as there is a lot of cases to handle

Emilio Jesús Gallego Arias (Jun 12 2022 at 12:55):

would be great to actually reduce what's allowed

Emilio Jesús Gallego Arias (Jun 12 2022 at 12:55):

that can go in parallel with the rest of the work

Emilio Jesús Gallego Arias (Jun 12 2022 at 12:56):

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 12:56):

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 12:56):

so actually less behaviors are allowed

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 12:57):

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

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?

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.

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

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?

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.

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:00):

There are several issues opened about it

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.

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

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?

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.

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.

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:04):

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:04):

There is just so much I can do

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.

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.

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_

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:06):

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

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:06):

cutting couple of seconds of a 30 mins build

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

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:07):

as it has to be buggy then

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.

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:09):

just the loading of deps makes coqdep take several seconds

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:09):

due to marshall

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 :)

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.

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

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?!

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:

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

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.

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:11):

and in this case you don't even need coqmod

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:11):

Coq can callback on Dune when Require is found

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:12):

Anyways I like coqdep

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:12):

coqmod sorry

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?

Rudi Grinberg (Jun 12 2022 at 13:12):

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

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:12):

nobody is questioning that

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

Rudi Grinberg (Jun 12 2022 at 13:13):

Is it not just a temporary state though?

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.

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:13):

Temporary is fine, but porting takes a few mins

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

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

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!

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:14):

Why do you care?

Ali Caglayan (Jun 12 2022 at 13:14):

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:14):

that's touching coqdep, not coqmod

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:14):

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:14):

why you want to work with buggy code then?

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:15):

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

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.

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:15):

Yes, that's why we have a CI

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:15):

and 2.5k bugs open

Ali Caglayan (Jun 12 2022 at 13:15):

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:15):

it won't eys

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:15):

it won't yes

Ali Caglayan (Jun 12 2022 at 13:15):

So why needlessly put users through this?

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:15):

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

Ali Caglayan (Jun 12 2022 at 13:16):

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

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?

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

Ali Caglayan (Jun 12 2022 at 13:16):

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:16):

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

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.

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:17):

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:17):

the grammar itself I mean

Ali Caglayan (Jun 12 2022 at 13:17):

We are not forking any grammar?

Ali Caglayan (Jun 12 2022 at 13:18):

The lexer is only 200 lines

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:18):

and if you have bugs, you can start fixing them

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.

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

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:19):

that's the main criteria

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:19):

so seems wise to start with that step

Ali Caglayan (Jun 12 2022 at 13:19):

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:19):

and be sure you have a lexer that works

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:20):

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

Ali Caglayan (Jun 12 2022 at 13:20):

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

Ali Caglayan (Jun 12 2022 at 13:20):

We can develop in dune and usptream later.

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:20):

Not in released code in Dune either

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:20):

so of course I'm talking about released code

Ali Caglayan (Jun 12 2022 at 13:20):

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

Ali Caglayan (Jun 12 2022 at 13:21):

It is an experiment that we would like to conduct.

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:21):

and what needs for it to be merged

Ali Caglayan (Jun 12 2022 at 13:21):

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:21):

Will you put coqmod in Dune's main branch?

Ali Caglayan (Jun 12 2022 at 13:21):

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

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?

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:22):

Seems like a bad plan to me

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:22):

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

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:23):

IIANM

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.

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:23):

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

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.

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:23):

and gives you very valuable testing

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:24):

so what's the argument against it?

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

Ali Caglayan (Jun 12 2022 at 13:24):

Don't fix what's not broken?

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:24):

So I'd love to see it upstreamed

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!

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.

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

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:26):

that's OK for me

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:26):

but actually coqmod has nothing else

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:26):

than the lexer

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:26):

why would you need to change the lexer for Dune?

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:26):

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

Ali Caglayan (Jun 12 2022 at 13:26):

This is slow

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:27):

Well, then keep your copy, fine

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:27):

but that copy can't be exposed to users

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 :)

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.

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.

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

Ali Caglayan (Jun 12 2022 at 13:29):

Let's get rid of it in a future PR

Ali Caglayan (Jun 12 2022 at 13:29):

That way we can test it there too.

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?

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.

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.

Rudi Grinberg (Jun 12 2022 at 13:30):

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

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

Ali Caglayan (Jun 12 2022 at 13:31):

Coqmod does no dep analysis!

Ali Caglayan (Jun 12 2022 at 13:31):

It just reports tokens that introduce deps

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.

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:31):

how is that different from dep analysis?

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.

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.

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:33):

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:33):

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

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:34):

of course you can experiment a lot

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

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:34):

it takes you 5 minutes

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:34):

and you get a lot of feedback on your lexer

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:35):

if it works, we can push it

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:35):

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:35):

you may choose to ignore it

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:35):

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:35):

you'll be in problems

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 —

Paolo Giarrusso (Jun 12 2022 at 13:36):

all the downsides you point out are real, of course

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

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:37):

and make dune-release work

Paolo Giarrusso (Jun 12 2022 at 13:37):

I also agree that incremental lexing is a distraction

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:37):

coqmod is great

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:37):

the discussion gets sidetracked all the time

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

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.

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

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

Paolo Giarrusso (Jun 12 2022 at 13:39):

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

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?

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!

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

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

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!

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

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.

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 ?

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:42):

who's blocking anything? (and how?)

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

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:43):

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

Paolo Giarrusso (Jun 12 2022 at 13:43):

good we agree here

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?

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.

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

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:44):

haha so I forgot how to count

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:44):

let's get rid of that stuff Gaëtan

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

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

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?

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.

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)

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 :(

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?

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.

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...

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:47):

also coqlib detection

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.

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.

Paolo Giarrusso (Jun 12 2022 at 13:48):

okay, that sounds like progress SwEng side!

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)

Ali Caglayan (Jun 12 2022 at 13:53):

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

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.

Rudi Grinberg (Jun 12 2022 at 13:54):

then we argue about what lives where

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:54):

@Ali Caglayan what does upstreaming to Dune mean?

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.

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:54):

(I bet there are more)

Ali Caglayan (Jun 12 2022 at 13:55):

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

Ali Caglayan (Jun 12 2022 at 13:55):

This is now about coqmod

Ali Caglayan (Jun 12 2022 at 13:55):

The other is about loadpath resolution

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)

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?

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

Ali Caglayan (Jun 12 2022 at 13:57):

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

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

We put the implementation of coqmod in dune's repo
We do not expose the binary to the user
We make a flag that enables the use of it. The old behavior is preserved otherwise

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

Rudi Grinberg (Jun 12 2022 at 13:59):

Because package managers suck. Opam especially so

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

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:59):

but it is up to you

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.

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:00):

or at least the lexer part

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

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.

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:00):

anyways I think the point is clear

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.