[library] Allow require to load libraries from memory.

[ejgallego]

This is one more step in our quest to avoid saving / loading .vo files to disk when not needed.

Most changes are straightforward except for the extension of the command type to include an internalization function.

This is IMHO a good start to the goal of having the vernacular layer access all file-system by a parameterized structure to interpretation, so document managers can properly handle file-system access.

For example, a typical use case in jsCoq is to download a .vo file on Require, but there are many more possibilities.

[ejgallego]

@coqbot run full CI

[SkySkimmer]

Considering how lib_resolver and dir are used I think it would make sense to have intern_file : string -> library_t
Then some upper layer would define

let intern_from_file dir =
  let f = Loadpath.try_locate_absolute_library dir in
  Feedback.feedback(Feedback.FileDependency (Some f, DirPath.to_string dir));
  let lib = Library.intern_file f in
  Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f));
  lib

(DirPath.equal dir lsd.md_name check left to intern_library as per my other comment)
(this would be done somewhere where we don't need to abstract over lib_resolver, I guess sysinit since stm depends on sysinit and sysinit needs this API)

[ejgallego]

It makes sense; we could just get rid of the Feedback.File stuff altogether (it was nice for jsCoq), as now users can just provide their own intern function, which should be usable for this.

This PR is usable for my purposes, however the Loadpath API is not.

[SkySkimmer]

@ejgallego ping

[gares]

The entire patch makes it possible to change the ~intern value at run time.

I don't see a use case, and we fix it once and for all at system initialization time, then this patch becomes much simpler, e.g. no need to changes to vernacextend.

Is there any use case for not having the intern function be given only once?

[gares]

simplify the patch making the intern argument part of the system configuration

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app]

This PR was not rebased after 30 days despite the warning, it is now closed.

[ejgallego]

The entire patch makes it possible to change the ~intern value at run time.

I don't see a use case, and we fix it once and for all at system initialization time, then this patch becomes much simpler, e.g. no need to changes to vernacextend.

Is there any use case for not having the intern function be given only once?

The main use case here is not so much to dynamically update the .vo intern function, but to follow a methodology where effects are reflected in the types of the commands. In this case, I'd like to have all the commands that require access to the env FS to reflect so in the type so the incremental engine can properly track these dependencies without having to analyze the internals.

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[SkySkimmer]

@gares at the coq call we could not figure out the need for your request for changes.
Please explain more, or alternatively we can merge as is (after rebase of course).

[gares]

It Is a matter of convenience and self documentation. Something set up at coq initialization time is supposed not to change, something you explicitly pass around may change but you pay the price of verbosity.

My last message was asking for use cases where the loader would change at run time. We're these provided in the call?

[ejgallego]

It Is a matter of convenience and self documentation.

How is it setting a global reference more convenient or better documented that declaring the effects a function perform in the type?

Something set up at coq initialization time is supposed not to change, something you explicitly pass around may change but you pay the price of verbosity.

My last message was asking for use cases where the loader would change at run time. We're these provided in the call?

There are use cases where the loader could change, but that's not the point of the current design, as I already explained above a few times.

Reading a .vo file is a side effect that needs to be tracked by the upper layers. It is good methodology to force commands accessing the filesystem to declare this access, so random commands cannot start reading .vo files for example without the upper layers being aware of it.

In this case the "price of verbosity" is pretty small, as compared to the gain of having a more principled API.

[gares]

So there are no concrete use cases you can cite.

[ejgallego]

So there are no concrete use cases you can cite.

My main use case is detecting which vernacular functions do read .vo files.

[gares]

This is not a use case.

[ejgallego]

This is not a use case.

Ok, if you don't want to call it "use case" is fine to me; but this is still an important need.

[SkySkimmer]

This argument about changing the value at runtime is nonsense, both a global ref and a passed parameter can do it.

[gares]

A global ref you set once at initialization time (the sysinit component) is not really a thing meant to be changed at runtime, even if ocaml let's you do it.

My impression from this discussion is that there is no need to pass the parameter, since it does not change while coq runs. If there was a usecase, I would prefer the explicit parameter.

Does it still sound like nonsense?

[ejgallego]

Does it still sound like nonsense?

You seem to focus on some criteria about refs vs parameter for things that change vs not. That's not the point of this PR.

The point of the technical solution chosen is to track which commands are going to access .vo reading, so that if a command needs to read a .vo, it has to declare it in the type.

This is an important need.

[SkySkimmer]

My impression from this discussion is that there is no need to pass the parameter, since it does not change while coq runs. If there was a usecase, I would prefer the explicit parameter.

I don't really understand the preference TBH.

Also I feel like this discussion should have been handled as "make suggestion for change -> Emilio rejects it because he really wants the parameter -> have it your way" instead of blocking the PR.

[coqbot-app]

This PR was not rebased after 30 days despite the warning, it is now closed.

[gares]

We can move on.

[andres-erbsen]

@gares FYI my understanding of what Emilio is trying accomplish using parameter-passing here is similar to visibility restrictions that have been broadly successful in simplifying code review. Whether the specific technical approach here is good or not, I don't know, but the overall concept has been quite valuable for me as a developer.

[ejgallego]

@andres-erbsen thanks for the reference. Indeed I do remain puzzled because the methodology we are using (isolation of state) is pretty standard in large systems.

Actually the origin of us making Coq command interpretation like this was motivated to write a modern document manager, project we started to study in 2016. We observed some key points:

• the vernac API is the main entry point for the document manager, and must be descriptive enough as to understand how commands affect state
• the most important feature for a document manager is incrementality
• the experience of Makarious Wenzel on turning Isabelle from a CLI tool to a modern UI showed that a functional model was required in order to make the implementation manageable
• our own experience with the number of bugs associated to Coq due to global state or wrong static analysis (very high)
• for UI development, incrementality is the most important feature
• incremental computing is pretty hard in the non-pure setting (see for example R. Leiven keynote on youtube)

Thus we aim to expose a vernac API that can reflect the effects the upper layers care about (in this case access to .vo files) in the types.

[ejgallego]

@ppedrot can you confirm this is correct w.r.t. the new Vmlibrary stuff?

[ppedrot]

I think so. Unrelatedly the dummy digest part is slightly more concerning to me, we should have an option there or something to signal that the data didn't come from a vo file.

[ppedrot]

(Also as-is this will never work with native, which is another reason why we should have a distinct library type.)

[ejgallego]

Let me indeed fix the digest stuff before this is merged.

Actually native could be made work with this in the same way: have the kernel relay a .cmxs request to the document manager / whoever is coordinating the filesystem layout.

Indeed it seems to me that a few parts of Coq could benefit from exposing a caching layer (that's the way I see the .vo files, as a cache), for example in #17674 ; I wanted to discuss this in the call actually.

[ppedrot]

Can we try to get this merged quickly before another flamewar roars up?

[ejgallego]

@ppedrot unfortunately it's gonna take me a while to rebase and test given my current workload; feel free to take over with the rebase + fixes due to upstream changes; I can do the testing myself.