Alex Sanchez-Stern (Feb 21 2023 at 19:58): Alex Sanchez-Stern (Feb 21 2023 at 19:58):Hey folks, does sertop have an equivalent to the coqc flag -noinit? I see that flag is used when compiling packages in coq's Init directory. The similarly named --no_init in sertop seems to be doing something with document manipulation, --no_prelude seems closer to what I want, but right now when I use it to run the contents of theories/Init/Logic.v it throws an error about not being able to eliminate SProp equality.
Gaëtan Gilbert (Feb 21 2023 at 19:59):can you post the error message?
Emilio Jesús Gallego Arias (Feb 21 2023 at 20:00):Hi @Alex Sanchez-Stern , there was a bug about not setting some kernel flag properly, what version are you using?
Emilio Jesús Gallego Arias (Feb 21 2023 at 20:01):See https://github.com/ejgallego/coq-serapi/pull/199
Emilio Jesús Gallego Arias (Feb 21 2023 at 20:01):If that's the fix, I'm very happy to give you commit access to SerAPI you can backport fixes to older versions (and happy to do newer opam releases as they are easy with dune-release tag + dune-release)
Alex Sanchez-Stern (Feb 21 2023 at 20:39):I'm working with coq 8.10 for this part (training on the version of coq from CoqGym). So it looks like it's before your pull request. I thought that wasn't the issue for a bit though, because I've gotten a different error message in the past for that issue. When I hit that issue before, I got the error: coq_serapy.CoqExn: SProp not allowed, you need to Set Allow StrictProp or to use the
-allow-sprop command-line-flag.. But this time the error message was coq_serapy.CoqExn: Cannot find the elimination combinator eq_sind, the elimination of the
inductive definition eq on sort SProp is probably not allowed., which made it seem like it was allowed to use SProps, but couldn't destruct them. It does seem like adding "Set Allow StrictProp." at the top of both files, plus the --no_prelude flag for Init/Logic.v, does the trick. I wouldn't say no to commit access to backport fixes though :).
Emilio Jesús Gallego Arias (Feb 21 2023 at 21:00):Yes, when the flag is off these eleminators are not generated, so I think indeed we should backport Vasily's PR to 8.10 then.
You should have an invite, feel indeed free to push PRs to any branch you'd like to see updated then.
Emilio Jesús Gallego Arias (Feb 21 2023 at 21:01):It's been a while since the 8.10 CI run, ping me on Github if you find any problem.
Emilio Jesús Gallego Arias (Feb 21 2023 at 21:01):Oh, actually 8.10 branch has already that fix backported I see
Emilio Jesús Gallego Arias (Feb 21 2023 at 21:03):oh never mind, I got it wrong, 8.10 doesn't have that PR, not sure if it should be there actually
Alex Sanchez-Stern (Feb 21 2023 at 21:09):What do you mean?
Emilio Jesús Gallego Arias (Feb 21 2023 at 21:09):I'm not sure if that setting was introduced in Coq 8.11 or Coq 8.10, need to check changelog
Alex Sanchez-Stern (Feb 21 2023 at 21:10):Ah, well the error message from 8.10 mentions "Allow StrictProp", is that the setting you mean?
Emilio Jesús Gallego Arias (Feb 21 2023 at 21:10):Indeed, https://coq.inria.fr/refman/changes.html#changes-in-8-11-beta1
Emilio Jesús Gallego Arias (Feb 21 2023 at 21:11):The setting was introduced in 8.10, but it was in 8.11 where it was made the default
Emilio Jesús Gallego Arias (Feb 21 2023 at 21:11):https://github.com/ejgallego/coq-serapi/pull/199 should not be in 8.10
Alex Sanchez-Stern (Feb 21 2023 at 21:13):Ah that makes sense.
Last updated: Apr 16 2024 at 18:02 UTC