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

[serlib] Explore ppx_override #759

Open
ejgallego opened this issue Sep 22, 2021 · 0 comments
Open

[serlib] Explore ppx_override #759

ejgallego opened this issue Sep 22, 2021 · 0 comments

Comments

@ejgallego
Copy link
Owner

Since the beginning, the manual override / re-export of Coq's type using ppx_import has been done manually [with the help of some hacky scripting]. It was planned to use a more methodical method in the future.

It turns out such as solution by @thierry-martinez exists, https://github.com/thierry-martinez/override should allow for a much more compact derivation of serializes for Coq's types.

ejgallego referenced this issue in ejgallego/opam-repository 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 rocq-archive/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 (rocq-archive/coq-serapi#249, fixes rocq-archive/coq-serapi#248, @Zimmi48, reported
            by @nyraghu)
 - [serapi] Fix COQPATH support: interpret paths as absolute (rocq-archive/coq-serapi#249, @Zimmi48)
 - [serlib] Ignore `env` parameter in certain exceptions (rocq-archive/coq-serapi#254, fixes rocq-archive/coq-serapi#250,
            @ejgallego, reported by @cpitclaudel)
 - [sertop] New option `--omit_env` that will disable the serialization of
            Coq's super heavy global environments (rocq-archive/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
@ejgallego ejgallego transferred this issue from rocq-archive/coq-serapi Jun 5, 2024
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

No branches or pull requests

1 participant