Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Set Firstorder Solver idtac. #317

Closed
andres-erbsen opened this issue Dec 27, 2022 · 1 comment · Fixed by #318
Closed

Set Firstorder Solver idtac. #317

andres-erbsen opened this issue Dec 27, 2022 · 1 comment · Fixed by #318
Labels

Comments

@andres-erbsen
Copy link
Contributor

Set Firstorder Solver idtac.
(*
There is no flag or option with this name: "Firstorder Solver idtac".
[unknown-option,option]
 *)
@whonore whonore added the bug label Dec 29, 2022
@whonore
Copy link
Owner

whonore commented Dec 29, 2022

The problem is the current solution of trying to guess the option value's type is pretty fragile. A better solution would be to get a list of all options and their types from Coq, but neither the GetOptions XML command nor Print Options seems to include Firstorder Solver. Two potential workarounds are to hardcode special cases for options that take tactic arguments (are there others?), or pass the whole command with Add instead of SetOptions and let Coq figure it out.

I'll take a look at what CoqIDE and VsCoq do and try to address this in the next couple days.

whonore added a commit that referenced this issue Dec 30, 2022
Rixxc pushed a commit to Rixxc/Coqtail that referenced this issue Jul 2, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants