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.
can you post the error message?
Hi @Alex Sanchez-Stern , there was a bug about not setting some kernel flag properly, what version are you using?
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)
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 :).
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.
It's been a while since the 8.10 CI run, ping me on Github if you find any problem.
Oh, actually 8.10 branch has already that fix backported I see
oh never mind, I got it wrong, 8.10 doesn't have that PR, not sure if it should be there actually
What do you mean?
I'm not sure if that setting was introduced in Coq 8.11 or Coq 8.10, need to check changelog
Ah, well the error message from 8.10 mentions "Allow StrictProp", is that the setting you mean?
The setting was introduced in 8.10, but it was in 8.11 where it was made the default
https://github.com/ejgallego/coq-serapi/pull/199 should not be in 8.10
Ah that makes sense.
Last updated: Jun 10 2023 at 23:01 UTC