Adapt to https://github.com/coq/coq/pull/19530

[proux01]

To be merged in sync with the upstream PR

[JasonGross]

To be merged in sync with the upstream PR

Coq Tools should not require synchronized merges; the bug minimizer needs to work across multiple versions of Coq. What's the issue?

[proux01]

To be merged in sync with the upstream PR

Coq Tools should not require synchronized merges; the bug minimizer needs to work across multiple versions of Coq. What's the issue?

Well, I guess we could have something backward compatible but here it's about backward compatibility with an old master thing that was never released, so probably not worth it.

[JasonGross]

Is this change actually necessary at this point? It breaks minimization on old versions of Coq. Maybe you meant to replace Stdlib with Coq below?

[JasonGross]

Example 048 fails because the code is minimized to something including Require Stdlib.Init.Ltac.

Example 055 is failing with "Error: Cannot find a physical path bound to logical path Prelude with prefix Stdlib." Any idea what's going wrong?

[JasonGross]

Example 055 is failing with "Error: Cannot find a physical path bound to logical path Prelude with prefix Stdlib."

I think we need to adjust

coq-tools/coq_tools/find_bug.py

Lines 2361 to 2364 in 6f29d5f

	if args.inline_prelude:
	for key in ("coqc_args", "coqtop_args", "passing_coqc_args", "passing_coqtop_args"):
	env[key] = tuple(list(env[key]) + ["-noinit"])
	inlined_contents = add_coqlib_prelude_import(inlined_contents, **env)

with a version check. Alternatively, we can move add_coqlib_prelude_import to be like

coq-tools/coq_tools/coq_running_support.py

Lines 26 to 60 in 6f29d5f

	def get_ltac_support_snippet(coqc, **kwargs):
	if coqc in LTAC_SUPPORT_SNIPPET.keys():
	return LTAC_SUPPORT_SNIPPET[coqc]
	test = r"""Inductive False : Prop := .
	Axiom proof_admitted : False.
	Tactic Notation "admit" := abstract case proof_admitted.
	Goal False. admit. Qed."""
	errinfo = {}
	native_ondemand_args = list(get_coq_native_compiler_ondemand_fragment(coqc, **kwargs))
	for before, after in (
	("Require Coq.Init.Ltac.\n", "Import Coq.Init.Ltac.\n"),
	("Require Coq.Init.Notations.\n", "Import Coq.Init.Notations.\n"),
	("Require Stdlib.Init.Ltac.\n", "Import Stdlib.Init.Ltac.\n"),
	("Require Stdlib.Init.Notations.\n", "Import Stdlib.Init.Notations.\n"),
	('Declare ML Module "coq-core.plugins.ltac".\n', ""),
	('Declare ML Module "coq-core.plugins.ltac".\n', 'Global Set Default Proof Mode "Classic".\n'),
	('Declare ML Module "ltac_plugin".\n', ""),
	('Declare ML Module "ltac_plugin".\n', 'Global Set Default Proof Mode "Classic".\n'),
	):
	contents = "%s\n%s\n%s" % (before, after, test)
	output, cmds, retcode, runtime = get_coq_output(
	coqc,
	tuple(["-q", "-nois"] + native_ondemand_args),
	contents,
	timeout_val=None,
	verbose_base=3,
	is_coqtop=kwargs["coqc_is_coqtop"],
	**kwargs,
	)
	if retcode == 0:
	LTAC_SUPPORT_SNIPPET[coqc] = (before, after)
	return (before, after)
	else:
	errinfo[contents] = {"output": output, "cmds": cmds, "retcode": retcode, "runtime": runtime}
	raise Exception("No valid ltac support snipped found. Debugging info: %s" % repr(errinfo))

[Zimmi48]

Example 055 is failing with "Error: Cannot find a physical path bound to logical path Prelude with prefix Stdlib." Any idea what's going wrong?

This can happen if you only depend on package rocq-core and not on coq-stdlib. Could that be the case?

Example 048 fails because the code is minimized to something including Require Stdlib.Init.Ltac.

If coq-stdlib is in scope, this should not be considered as a failure (unless coq-stdlib is now viewed as an external library which makes the test fail).

[proux01]

example55 works locally so I guess Theo is right and this is a CI issue. This is probably waiting for the Docker image

[JasonGross]

Example 048 fails because the code is minimized to something including Require Stdlib.Init.Ltac.

If coq-stdlib is in scope, this should not be considered as a failure (unless coq-stdlib is now viewed as an external library which makes the test fail).

Right, this is just a regex that needs fixing, I've committed the fix

[erikmd]

@Zimmi48

Example 055 is failing with "Error: Cannot find a physical path bound to logical path Prelude with prefix Stdlib." Any idea what's going wrong?

FYI this looks like the same error we get in building coqorg/coq:dev in Docker-Coq — Bignums does not find the Stdlib anymore since the recent coq-stdlib-related changes.

after a bit of investigation and discussion with @proux01, it appears
https://github.com/coq/opam/blob/master/core-dev/packages/coq-stdlib/coq-stdlib.dev/opam is broken: after doing opam install coq-stdlib.dev, no .vo from coq-stdlib is installed anymore.

I tested an alternative version of this .opam file, to no avail:

opam-version: "2.0"
synopsis: "The Coq Proof Assistant -- Standard Library"
description: """
Coq is a formal proof management system. It provides
a formal language to write mathematical definitions, executable
algorithms and theorems together with an environment for
semi-interactive development of machine-checked proofs.

Typical applications include the certification of properties of
programming languages (e.g. the CompCert compiler certification
project, or the Bedrock verified low-level programming library), the
formalization of mathematics (e.g. the full formalization of the
Feit-Thompson theorem or homotopy type theory) and teaching.

This package includes the Coq Standard Library, that is to say, the
set of modules usually bound to the Stdlib.* namespace."""
maintainer: ["The Coq standard library development team"]
authors: ["The Coq development team, INRIA, CNRS, and contributors"]
license: "LGPL-2.1-only"
homepage: "https://coq.inria.fr/"
doc: "https://coq.github.io/doc/"
bug-reports: "https://github.com/coq/coq/issues"
depends: [
  "dune" {>= "3.8"}
  "coq-core"
  "rocq-core" {= version}
  "odoc" {with-doc}
]
depopts: ["coq-native"]
dev-repo: "git+https://github.com/coq/coq.git"
# man dune (3.16.1)
# "-p" name :=
# "--release" "--only-packages" name :=
# "--root" "." "--ignore-promoted-rules" "--no-config" "--profile" "release"
# "--always-show-command-line" "--promote-install-files"
# "--require-dune-project-file" "--ignore-lock-dir"
# "--default-target" "@install" "--only-packages" name
build: [
  ["dune" "subst"] {dev}
  [
    "dune"
    "build"
    "--root" "stdlib" "--ignore-promoted-rules" "--no-config"
    "--profile" "release" "--always-show-command-line"
    "--require-dune-project-file" "--ignore-lock-dir"
    "--default-target" "@install" "--only-packages" name
    "-j"
    jobs
    "--promote-install-files=false"
    "@install"
    "@runtest" {with-test}
    "@doc" {with-doc}
  ]
  ["dune" "install" "--root" "stdlib" "--ignore-promoted-rules" "--no-config"
   "--profile" "release" "--always-show-command-line"
   "--promote-install-files" "--require-dune-project-file" "--ignore-lock-dir"
   "--default-target" "@install" "--only-packages" name
   "--create-install-files" name]
]

url {
  src: "git+https://github.com/coq/coq.git#master"
}

so @proux01 should investigate further on this Monday

[proux01]

Sorry for the delay, the opam/docker issue is now fixed and CI seems happy, can this be merged?

[proux01]

Thanks for your patience!