search

cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
228 stars 36 forks source link

Use module names rather than file names for output #25

Open JasonGross opened 3 years ago

JasonGross commented 3 years ago

Fixes #14

Code adjusted from https://github.com/JasonGross/coq-tools/blob/9b81719a2172e4301126378e5aebf83e3f2b43e6/import_util.py#L99-L111

cpitclaudel commented 3 years ago

Thanks a lot, Jason. Is there no way for SerAPI to give us this information? I'm wary of adding code that I don't understand fully, and that (I think?) duplicates something that Coq already does internally.

Maybe @ejgallego can help? Emilio, we'd like to name the files produced by Alectryon based on their module path; can SerAPI tell us what the module path of the current file is? Thanks!

ejgallego commented 3 years ago

Maybe @ejgallego can help? Emilio, we'd like to name the files produced by Alectryon based on their module path; can SerAPI tell us what the module path of the current file is?

Yes it can as the logic is already there, I'm not sure if exposed in the protocol, but should be very easy to add. So IUUC you want the function at https://github.com/coq/coq/blob/ea62d1e19f2ba565ea3a18ba3709a06af5c845ac/sysinit/coqargs.ml#L459 exposed in the API? Should be a matter of just wrapping it.

Note that there has been a lot of work in providing a better setup for Coq libraries and theories, including a single, queryable API for loadpaths etc... , but it is still not finished, but that doesn't mean we forgot about it and other requests.

ejgallego commented 3 years ago

Note that there has been a lot of work in providing a better setup for Coq libraries and theories, including a single, queryable API for loadpaths etc... , but it is still not finished, but that doesn't mean we forgot about it and other requests.

In particular a terrible pitfall current tooling for Coq has is that it has several copies of code managing COQPATH, -R, -Q ,etc ... and not only that, the copies differ on the semantics [for example coqchk does not interpreter -R / -Q the same]

A fix for this is already started at https://github.com/coq/coq/pull/14059 , but indeed note that I strongly discourage people doing tooling having their own logic for loadpaths, instead they should aim to use the existing code and the new library as soon as it is available.

I say this because it is extremely likely that there will big changes in how libs are managed in Coq in the short term, so any code you write for that today will not work soon unless you indeed use the API we aim to provide in coq-core.boot , which will provide compatibility.

In particular, it is not safe to make any assumptions on paths [which are opaque on the new library] and on mappings w.r.t. paths <-> dirmaps.

ejgallego commented 3 years ago

Added , c.f. https://github.com/ejgallego/coq-serapi/pull/236/files

[Note the function was already there but unused, I got side-tracked sadly but indeed there were plans to expose it]

JasonGross commented 3 years ago

@cpitclaudel do you want me to update this PR with your feedback, or shall we abandon it in favor of https://github.com/ejgallego/coq-serapi/pull/236? (I imagine it'd be easy for you to code something up using that?)

@ejgallego

I say this because it is extremely likely that there will big changes in how libs are managed in Coq in the short term, so any code you write for that today will not work soon

I'm not sure what to make of this, given that I maintain https://github.com/JasonGross/coq-tools to be compatible with Coq all the way back to 8.5. (I dropped 8.4 when it got too hard to build on newer versions of Linux.) Are people's developments going to suddenly start breaking? Or are you just saying that the edge cases are going to change behavior?

ejgallego commented 3 years ago

I'm not sure what to make of this, given that I maintain https://github.com/JasonGross/coq-tools to be compatible with Coq all the way back to 8.5. (I dropped 8.4 when it got too hard to build on newer versions of Linux.) Are people's developments going to suddenly start breaking? Or are you just saying that the edge cases are going to change behavior?

Hard to know yet, the proposal is not even in CEP form. So indeed the current model will be "V1 library model" and I think it will keep working for a while, for users of the new features, coq-tools would indeed require likely a lot of work. So it is more about additional features than about the existing model which will be preserved, but indeed some stuff such as concrete file location may change. Easy example: we will stop installing everything under lib/coq/user-contrib.

IMHO we should try to avoid placing duplicate logic inside tooling, but rather take the painful but correct path which it is to have the tooling use the right upstream libraries instead. Updated SerAPI protocol will hopefully come with direct Python bindings so for Coq tools it should be a matter of using the Python API I hope.

Tradeoffs are subtle here tho, a typical example is parsing. Many people have tried to re-implement Coq's parser (with not the best results IMO), where in most cases the right solution indeed is to use Coq's parser, however Coq parsing API is not good for all use cases so YMMV.

For now my idea is to support Python, OCaml, and JavaScript/TypeScript users in direct API form, rest are on their own with the serialized RPC . Reimplementing any kind of logic separately IMHO leads to inevitable bitrot, as either:

ejgallego commented 3 years ago

As for this PR I guess the best tradeoff is to keep the Python code in a compat module, and use it if SerAPI < supported version, otherwise use the SerAPI tool.

This kind of "polyfill" pattern could be useful for some other features IMHO.

ejgallego commented 3 years ago

Now that I have hijacked the thread and we are talking about what the protocol can/should do I'd like to do a very brief update on what is the status w.r.t. things Alectryon needs: the short story is that after analyzing what is missing for Alectryon, unfortunately to implement/provide that properly does require deep changes in the way we handle documents internally in Coq; a presentation of what is going on should hopefully happen soon.

JasonGross commented 3 years ago

Tradeoffs are subtle here tho, a typical example is parsing. Many people have tried to re-implement Coq's parser (with not the best results IMO), where in most cases the right solution indeed is to use Coq's parser, however Coq parsing API is not good for all use cases so YMMV.

My solution to this was to run coqtop -time -emacs and let Coq parse things into sentences with character locations. And then I discovered even this is not perfect, because coqtop -time gives locations in bytes, whereas python3 uses characters...

ejgallego commented 3 years ago

My solution to this was to run coqtop -time -emacs and let Coq parse things into sentences with character locations. And then I discovered even this is not perfect, because coqtop -time gives locations in bytes, whereas python3 uses characters...

That's an easy case, if you are already running coqc then you can use the coq parser or sercomp very easily. The main pitfall of Coq's parser is that actually it will run documents, so if a proof fails then you miss the rest of the parsetree of the document often.

IMVHO this is poorly managed by current Coq implementation, new document managers should make this much better but still parsing is tied to execution so if you need a truly isolated parsing phase you are out of luck and will have to write your own :(

cpitclaudel commented 3 years ago

@cpitclaudel do you want me to update this PR with your feedback, or shall we abandon it in favor of ejgallego/coq-serapi#236? (I imagine it'd be easy for you to code something up using that?)

I think I prefer that solution in the long term. While we wait for that we could work on this PR, but I think it would work very nicely as well to just monkey-patch things on your side. WDYT?

cpitclaudel commented 3 years ago

As for this PR I guess the best tradeoff is to keep the Python code in a compat module, and use it if SerAPI < supported version, otherwise use the SerAPI tool.

We could, but that's more maintenance and more debugging. I prefer to take a dependency on a more recent SerAPI.

cpitclaudel commented 3 years ago

unfortunately to implement/provide that properly does require deep changes in the way we handle documents internally in Coq; a presentation of what is going on should hopefully happen soon.

Got it, thanks a lot for the update!

cpitclaudel commented 3 years ago

And then I discovered even this is not perfect, because coqtop -time gives locations in bytes, whereas python3 uses characters...

You can easily translate between these two, I think, as long as each of the cutoffs is between codepoints. (basically you split the bytestring at positions reported by Coq, then encode each sub-bytestring and compute cumulative sums over the lengths of the resulting (sub)strings). But indeed this is a case where sercomp is pretty nice.

ejgallego commented 3 years ago

We could, but that's more maintenance and more debugging. I prefer to take a dependency on a more recent SerAPI.

Sounds good, let me then review my org file to see what more patches I have pending for Alectryon and I'll make a SerAPI release this week.

ejgallego commented 3 years ago

But indeed this is a case where sercomp is pretty nice.

And much faster than coqc usually as it has a parsing-only mode.

JasonGross commented 3 years ago

You can easily translate between these two, I think, as long as each of the cutoffs is between codepoints. (basically you split the bytestring at positions reported by Coq, then encode each sub-bytestring and compute cumulative sums over the lengths of the resulting (sub)strings). But indeed this is a case where sercomp is pretty nice.

I think the bigger problem is that I'm trying to be compatible with both python 2 and python 3, and they handle strings in different ways.

cpitclaudel commented 3 years ago

I think the bigger problem is that I'm trying to be compatible with both python 2 and python 3, and they handle strings in different ways.

That's software archeology: Python 2 has been EOL for 10 years and unsupported for since last year :)

JasonGross commented 3 years ago

@cpitclaudel do you want me to update this PR with your feedback, or shall we abandon it in favor of ejgallego/coq-serapi#236? (I imagine it'd be easy for you to code something up using that?)

I think I prefer that solution in the long term. While we wait for that we could work on this PR, but I think it would work very nicely as well to just monkey-patch things on your side. WDYT?

I'm happy to just depend on my fork of alectryon until the better long term fix happens, assuming it'll happen in the not-too-distant future.

Alizter commented 7 months ago

@JasonGross Any chance you can update your fork? It is lagging behind and we need newer alectryon features for HoTT.

JasonGross commented 7 months ago

@cpitclaudel What is the status of the more principled fix here?

JasonGross commented 7 months ago

@Alizter I've rebased.

cpitclaudel commented 6 months ago

Sorry, I missed this message because my Coq filter was too aggressive (looks like I missed a lot of stuff) :/

@cpitclaudel What is the status of the more principled fix here?

It seems that it got merged! So we should probably use that.

But, re-reading #14 , it seems that what -base in coq2html does is much simpler; or did I miss something? It looks like it ignores all -Q, etc and the user just specified explicitly?

JasonGross commented 6 months ago

But, re-reading #14 , it seems that what -base in coq2html does is much simpler; or did I miss something? It looks like it ignores all -Q, etc and the user just specified explicitly?

Where is the implementation of -base in coq2html?

cpitclaudel commented 6 months ago

Where is the implementation of -base in coq2html?

It's described here: https://github.com/xavierleroy/coq2html?tab=readme-ov-file#html-generation

It's completely trivial; it just prepends its argument to the name of each generated file:

https://github.com/xavierleroy/coq2html/blob/0bf6739766ac5ca64c54e97324b60b46be96568a/coq2html.mll#L437

JasonGross commented 6 months ago

But, re-reading #14 , it seems that what -base in coq2html does is much simpler; or did I miss something? It looks like it ignores all -Q, etc and the user just specified explicitly?

Where is the implementation of -base in coq2html?

It's described here: https://github.com/xavierleroy/coq2html?tab=readme-ov-file#html-generation

It's completely trivial; it just prepends its argument to the name of each generated file:

https://github.com/xavierleroy/coq2html/blob/0bf6739766ac5ca64c54e97324b60b46be96568a/coq2html.mll#L437

Ah, yes, it looks like -base is much simpler and should solve #14