Rocq CLI #19927
Merged
Rocq CLI #19927
+4,305
−3,386
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Executable `rocq` can be called as `rocq compile args` (also `rocq c args`) and will in turn call `coqworker --kind=compile args`. (coqworker will be renamed later) coqc has also been modified to call coqworker. The design where `rocq` calls the worker executable instead of being itself the worker executable is so that `rocq check` can work without involving the main worker code. We could also consider not having `rocq` handle `rocqchk` ie keeping it completely separate. TODO: - make rocq handle coqtop mode - make coqtop use the worker - make rocq handle coqnative mode - make coqnative use the worker(?) - make rocq handle coqchk mode(?) - make rocq handle misc modes (makefile, dep, doc, maybe tex, workmgr, votour?) - make rocq handle coqidetop mode(?) - make coqidetop use the worker(?) this would mean the worker depends on the xml protocol - make rocq handle coqide mode(?) Issues to be solved: - (if coqtop.byte is to use the worker): figure out how to support coqtop.byte's extensions (dependency on coq-core.dev for printers, compiler-libs, findlib.top) without impacting worker.byte in non-coqtop modes
…ore`
Not sure if `chdir %{project_root}` is correct or if it should be
`%{workspace_root}` (this only matters for error messages).
rocq compile will handle it
Zimmi48
reviewed
Dec 12, 2024
coqbot-app
bot
added
the
needs: full CI
SkySkimmer
added
the
request: full CI
coqbot-app
bot
removed
request: full CI
SkySkimmer
added
the
request: full CI
coqbot-app
bot
removed
the
request: full CI
SkySkimmer
added
the
request: full CI
coqbot-app
bot
removed
the
request: full CI
ejgallego
added a commit
to SkySkimmer/coq-lsp
that referenced
this pull request
Dec 13, 2024
Co-authored-by: Emilio Jesús Gallego Arias <[email protected]>
ppedrot
approved these changes
Dec 18, 2024
|
@coqbot merge now |
|
@ppedrot: Please take care of the following overlays:
|
SkySkimmer
added a commit
to ejgallego/coq-lsp
that referenced
this pull request
Dec 18, 2024
Adapt to coq/coq#19927 (coq-core renamed to rocq-runtime)
SkySkimmer
added a commit
to coq-community/coq-dpdgraph
that referenced
this pull request
Dec 18, 2024
Adapt to coq/coq#19927 (coq-core renamed to rocq-runtime)
3 tasks
This was referenced Dec 20, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Replace #19764 to drop the history of pushes in the github interface
summary:
plan for a followup PR
Under the hood, the smaller subcommands are statically linked in
rocq, and compile/repl/repl-with-drop/native-precompile use separate workers.This mostly works out to anything needing the kernel being split to a separate executable.
rocqchkandvotourcan be accessed both throughrocq(rocq checkandrocq votourrespectively) and as separate executables (rocq just calls the separate exe).For rocqchk this is particularly meaningful since it means we don't need to inspect rocq (including all the subcommands statically linked in) to trust it.
For votour it's mostly because the executable name doesn't conflict with
rocq. We could move it to a private exe called throughrocq votouror keep it public and drop therocq votoursubcommand if we wanted.rocqis in packagerocq-runtime.coq-corestill exists and contains compat binaries coqc etc (the compat binaries use the rocq-runtime worker if there is one).Todo in followup PRs:
manpage for rocqOverlays: