You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
It seems useful to collect instances of the bug minimizer being used, since I'm hopeful @achlipala and @Zimmi48 and I will be able to get a paper out of this.
Automatic bidirectionality hints coq/coq#13107 (comment) (ci-tlc, using symlinks rather than matching paths exactly when rebuilding the ci target resulted in the .v.d files pointing to the wrong dependencies, resulting in non-deterministic build orders and trying to build files before their dependencies finished; fixed by c5073ca)
Automatic bidirectionality hints coq/coq#13107 (comment) (ci-coq_performance_tests, Error: /github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/../coq-core/kernel/nativevalues.cmi is not a compiled interface for this version of OCaml., failure to run eval $(opam env) in the right place, finally fixed by 8244ace)
It seems useful to collect instances of the bug minimizer being used, since I'm hopeful @achlipala and @Zimmi48 and I will be able to get a paper out of this.
Here are uses so far:
Reflexive
to have mode! !
coq/coq#13969 (comment) (ci-mathcomp, 39m (May 24, 8:34 AM -- 9:13 AM))Reflexive
to have mode! !
coq/coq#13969 (comment) (ci-iris, 35m (May 26, 6:59 PM -- 7:34 PM))Reflexive
to have mode! !
coq/coq#13969 (comment) (ci-quickchick, 9m (May 26, 10:10 AM -- 10:19 AM))Reflexive
to have mode! !
coq/coq#13969 (comment) (ci-equations, 9m (May 27, 12:06 PM -- 12:15 PM))Reflexive
to have mode! !
coq/coq#13969 (comment) (ci-perennial, 32m (May 28, 10:26 AM -- 10:58 AM))Reflexive
to have mode! !
coq/coq#13969 (comment) (ci-fourcolor, 40m (May 28, 4:18 PM -- 4:58 PM))To get another of these lines:
Reactions to minimization:
Reflexive
to have mode! !
coq/coq#13969 (comment)Early speedbumps and non-uses:
Require
s around)filename_of_lib
now prefers existing files JasonGross/coq-tools#66)Reflexive
to have mode! !
coq/coq#13969 (comment) (ci-mathcomp, download issue?)Reflexive
to have mode! !
coq/coq#13969 (comment) (ci-iris coqchk anomaly)Reflexive
to have mode! !
coq/coq#13969 (comment) (ci-equations, mismatch between character locations and byte locations)Reflexive
to have mode! !
coq/coq#13969 (comment) (ci-fourcolor,\r\n
line endings on Linux)Reflexive
to have mode! !
coq/coq#13969 (comment) (ci-perennial, perennial passed-noglob
, fixed by Revert a57832ec6f4a43c184151f4a962b296d0e1cc982 and remove-noglob
mit-pdos/perennial#35)-o
arguments to coqc)Error: Universe {tmppwdtukmb.112} is unbound.
does not matchError: Universe {TestSuite.issues.issue7.110} is unbound.
)^*
plus(x^*)
showing up, fixed by JasonGross/coq-tools@f3c3d32)IFS
was set wrong forCOQPATH
handling, fixed by 2d6e1f4)Module
s fails due to bugs in Coq'sImport
semantics JasonGross/coq-tools#67, should be fixed by JasonGross/coq-tools@74f06c5)eval $(opam env)
in the right place, finally fixed by 8244ace)-dump-glob
, fixed by 6272027)Inductive False
gains a universe when put after inlined modules; see ForceFalse
axiom inProp
JasonGross/coq-tools#75,False
inductive sensitive to universe polymorphism, resulting inadmit
ed definitions being sensitive to universe polymorphism setting JasonGross/coq-tools#74, and Universe errors inDefined
misreport error location coq/coq#15073 for more details)Load
results in miscomputed / misused glob file, see .glob files are incorrect (and result in incorrect html linking) whenLoad
is used coq/coq#15497, fixed by Be more robust in absolutizing files JasonGross/coq-tools#104)The command has indeed failed with message
as an error, fixed by JasonGross/coq-tools@abedb0e)Goal
statements fail to be removed becausecoqc -time
does not report times forAbort
statement and this messes up parsing, cfcoqc -time
fails to report times forAbort
coq/coq#15666)Not yet diagnosed, but unable to reproduce from the artifact:
Not yet fixed:
intuition
behavior as a result ofRequire
side effects)Import
incorrectly imports printing notations which are not present when the module is open coq/coq#14587)CoLoR.Util.Set.*
cannot be inlined becauseModule Set
is not valid Coq, CoLoR cannot be minimized by the bug minimizer due to folderSet
fblanqui/color#34)destruct net
followed bydestruct nwState
; reported as Please do not depend on autogenerated names ofdestruct
that are sensitive to the file in which records are defined uwplse/verdi#130)Obligation Tactic := ...
followsRequire
, cfObligation Tactic
should support#[export]
attribute, and should default to#[export]
rather than#[global]
coq/coq#15072, results in change of obligation tactic behavior)normalize_requires
messing up compilation success:In process of fixing
Require
after the the buggy line)Not yet diagnosed:
PR for testing ci minimization: coq/coq#14328, now coq/coq#14579
The text was updated successfully, but these errors were encountered: