Skip to content

Fix repeated Coqargs parsing with ~init - #22334

Open
finalchild wants to merge 1 commit into
rocq-prover:masterfrom
finalchild:agent/coqargs-compositional-parsing
Open

Fix repeated Coqargs parsing with ~init#22334
finalchild wants to merge 1 commit into
rocq-prover:masterfrom
finalchild:agent/coqargs-compositional-parsing

Conversation

@finalchild

@finalchild finalchild commented Aug 8, 2026

Copy link
Copy Markdown

Problem

Coqargs.parse_args accepts an existing option value through ~init (also exposed as
Coqinit.parse_arguments ~initial_args). A value returned by one call should therefore be valid
input to a later call. Currently it is not.

The parser builds ordered list fields by prepending, and the public wrapper reverses those fields
before returning them. On a later call, the already-normalized init value is treated as if it
were still in the parser's reverse-accumulator representation. The wrapper then reverses the
whole result again. Consequently, even parsing an empty argument list can reorder options that
were already present.

-package has an additional problem: every parse resolves the complete accumulated package list
and inserts the resulting load paths into vo_includes. Calling the parser again can therefore
resolve old packages again and mix duplicate derived paths with explicit -Q/-R paths.

This is a correctness bug in the existing ~init API, rather than an API refactoring.

Impact

Load-path order determines precedence when physical paths or logical prefixes overlap. Clients
that parse arguments in layers can therefore resolve a .vo file through a different mapping
than a one-pass command-line invocation.

VsRocq does this when it combines project and process/document arguments. With Dune projects with (generate_project_file),
reordering the project-root mapping and the _build/default mapping can make Rocq assign the wrong
logical name to a compiled file, producing errors of the form:

The file .../_build/default/LibSepReference.vo contains library
SLF.LibSepReference and not library SLF._build.default.LibSepReference.

Other embedders using Coqargs.parse_args ~init or
Coqinit.parse_arguments ~initial_args are affected by the same ordering and repeated-resolution
behavior.

Fix

  • Treat values at the public parse_args boundary as normalized, in correct declaration order. Thus, reverse the lists also in the beginning, not only in the end.
  • Keep raw package names in pre.packages while parsing. Resolve them once in init_document, at
    the point where package load paths are installed.
  • Move the rocq-runtime.lib dependency from the coqargs library to sysinit, following the
    move of Rocq_package.resolve call.

Resolving only packages newly seen by each parser call was considered, but would leave parsing
dependent on Findlib state and require tracking which package closures had already been expanded.
Deferring resolution keeps parsing repeatable and gives package expansion a single owner.

Compatibility

There is no type or record-shape change. The intended behavior changes are observable, however:

  • ordered fields, including pre.packages, are now consistently returned in declaration order (corrected behavior);
  • immediately after Coqargs.parse_args, pre.vo_includes contains only explicit -Q/-R
    entries, not paths derived from -package (field semantic changes);
  • a missing package is reported by init_document rather than by argument parsing.

The normal Coqinit startup path already initializes the document, so it receives the same
package load paths at the correct stage. A downstream caller that uses Coqargs.parse_args
directly and expects package-derived entries in pre.vo_includes before document initialization
will need to adjust to the new resolution point. This is the principal downstream compatibility
risk.

Tests

  • A new coqargs unit test compares one-pass parsing with two calls joined through ~init, checks
    that an empty incremental parse is an identity, verifies declaration order for all accumulator
    fields, and verifies that parsing does not resolve a nonexistent package.
  • misc/rocq-find.sh now exercises the new resolution point end to end: a package and its
    transitive dependency are compiled and loaded through -package, and a missing package must
    still fail during document initialization.

AI disclaimer

AI debugged the issue, human discussed the fix direction with AI, AI wrote the code and PR, and human reviewed them. I'm not good at shell scripts, so please check whether the test script is good enough.

@coqbot-app coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Aug 8, 2026
@finalchild
finalchild force-pushed the agent/coqargs-compositional-parsing branch 5 times, most recently from 4eb43a1 to bbb67a8 Compare August 8, 2026 17:22
@finalchild finalchild changed the title Make Coqargs parsing compositional Fix repeated Coqargs parsing with ~init Aug 8, 2026
@finalchild
finalchild marked this pull request as ready for review August 8, 2026 17:43
@finalchild
finalchild requested review from a team as code owners August 8, 2026 17:43
Coqargs.parse_args returns ordered list fields, but a returned value reused
as init was treated as a reverse-order accumulator. This could reorder
existing options. Package declarations were also resolved on every parse,
potentially inserting derived load paths repeatedly.

Normalize init before entering the parser and normalize the result afterward.
Keep package declarations unresolved until init_document so package load
paths are installed once at their point of use.
@finalchild
finalchild force-pushed the agent/coqargs-compositional-parsing branch from bbb67a8 to 29ae900 Compare August 8, 2026 17:45
@SkySkimmer

Copy link
Copy Markdown
Contributor

see also #22259

@finalchild

Copy link
Copy Markdown
Author

see also #22259

I'll rebase on it once it's merged. This PR can then focus on fixing the reversal.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants