Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use module names rather than file names for output #25

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

JasonGross
Copy link
Contributor

alectryon/cli.py Outdated Show resolved Hide resolved
@cpitclaudel
Copy link
Owner

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!

# will result in confusing names if the path starts with '..', so
# in that case we use the absolute path
fpath = os.path.relpath(os.path.normpath(fpath), '.')
if fpath.startswith('..' + os.sep) and not os.path.abspath(fpath): # do we need the second conjunct ever?
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can this branch ever be taken? That is, when does not os.path.abspath(fpath) return True?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the not os.path.abspath(fpath) is redundant because paths starting with ../ should never be absolute (absolute means that it starts with a mount point/drive letter or else starts with /, I think). But the branch is certainly taken, for example if you invoke the script on ../foo.v

alectryon/cli.py Outdated
return lambda contents, fname, output, output_directory: \
write_output(ext, contents, fname, output, output_directory)
return lambda contents, fname, fpath, output, output_directory, coq_args_Q, coq_args_R: \
write_output(ext, contents, fname, fpath, output, output_directory, coq_args_Q, coq_args_R)
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't this transformation only happen for Coq files? Presumably reST file don't need the renaming, right?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think that files should either be module-named or else laid out in a directory hirerachy. Are all non-coq files flat? (And what about .v.rst?).

alectryon/cli.py Outdated Show resolved Hide resolved
@ejgallego
Copy link

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
Copy link

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 coq/coq#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 added a commit to ejgallego/coq-serapi that referenced this pull request Apr 13, 2021
Coq's library handling code contains an API to map "logical" paths to
"physical" paths and vice-versa, we provide a helper query

```lisp
(Query () (LogicalPath file))
```

which exposes this resolution for users, as requested in
cpitclaudel/alectryon#25

Note that the plan for 8.14 is to expose the fully principled API that
will be introduced at coq/coq#14059.
@ejgallego
Copy link

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
Copy link
Contributor Author

@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?)

@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
Copy link

ejgallego commented Apr 13, 2021

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:

  • Coq is developing at a healthy pace, which means a lot of stuff will evolve and be hard to track
  • Coq is not developing fast, which signals other problems then.

@ejgallego
Copy link

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
Copy link

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
Copy link
Contributor Author

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
Copy link

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
Copy link
Owner

@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
Copy link
Owner

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
Copy link
Owner

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
Copy link
Owner

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
Copy link

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
Copy link

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
Copy link
Contributor Author

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
Copy link
Owner

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
Copy link
Contributor Author

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

ejgallego added a commit to ejgallego/coq-serapi that referenced this pull request Apr 17, 2021
Coq's library handling code contains an API to map "logical" paths to
"physical" paths and vice-versa, we provide a helper query

```lisp
(Query () (LogicalPath file))
```

which exposes this resolution for users, as requested in
cpitclaudel/alectryon#25

Note that the plan for 8.14 is to expose the fully principled API that
will be introduced at coq/coq#14059.
@cpitclaudel cpitclaudel force-pushed the master branch 3 times, most recently from 458fba8 to ebfdc34 Compare August 5, 2021 07:14
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Jun 15, 2022
CHANGES:

 - [serapi] New query `(Query () (LogicalPath file))` which will
            return the logical path for a particular `.v` file
            (@ejgallego, see also
            cpitclaudel/alectryon#25)
 - [serapi] new `(SaveDoc opts)` command supporting saving of .vo
            files even when from interactive mode; note that using
            `--topfile` is required (fixes ejgallego/coq-serapi#238, @ejgallego, reported
            by Jason Gross)
 - [sertop] we don't link the OCaml `num` library anymore, this could
            have some impact on plugins (@ejgallego)
 - [nix]    Added Nix support (ejgallego/coq-serapi#249, fixes ejgallego/coq-serapi#248, @Zimmi48, reported
            by @nyraghu)
 - [serapi] Fix COQPATH support: interpret paths as absolute (ejgallego/coq-serapi#249, @Zimmi48)
 - [serlib] Ignore `env` parameter in certain exceptions (ejgallego/coq-serapi#254, fixes ejgallego/coq-serapi#250,
            @ejgallego, reported by @cpitclaudel)
 - [sertop] New option `--omit_env` that will disable the serialization of
            Coq's super heavy global environments (ejgallego/coq-serapi#254 @ejgallego)
 - [build]  Test OCaml 4.12 (ejgallego/coq-serapi#257 @ejgallego)
 - [sertop] Async mode was not working due to passing `-no-glob` to workers
@Alizter
Copy link

Alizter commented Feb 9, 2024

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

@JasonGross
Copy link
Contributor Author

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

@JasonGross
Copy link
Contributor Author

@Alizter I've rebased.

@cpitclaudel
Copy link
Owner

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
Copy link
Contributor Author

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
Copy link
Owner

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
Copy link
Contributor Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Collision between generated HTML filenames
4 participants