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

Better control over ltac backtraces #7769

Closed
RalfJung opened this issue Jun 10, 2018 · 3 comments · Fixed by #9142

Comments

@RalfJung
Copy link
Contributor

commented Jun 10, 2018

Version

8.8.0

Operating system

Linux

Description of the problem

When using a tactic the wrong way in the Iris proof mode, we are frequently presented with error messages like this:

The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)", "iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializePat (open_constr) (constr)" and "go" (bound to
fun H1 pats =>
  lazymatch pats with
  | [] => idtac
  | spec_patterns.SForall :: ?pats =>
      idtac "[IPM] The * specialization pattern is deprecated because it is applied implicitly.";
       go H1 pats
  | spec_patterns.SIdent ?H2 :: ?pats =>
      notypeclasses refine (coq_tactics.tac_specialize _ _ _ H2 _ H1 _ _ _ _ _ _ _ _ _ _);
       [ env_reflexivity || fail "iSpecialize:" H2 "not found"
       | env_reflexivity || fail "iSpecialize:" H1 "not found"
       | iSolveTC ||
           (let P := match goal with
                     | |- IntoWand _ _ ?P ?Q _ => P
                     end in
            let Q := match goal with
                     | |- IntoWand _ _ ?P ?Q _ => Q
                     end in
            fail "iSpecialize: cannot instantiate" P "with" Q)
       | env_reflexivity
       | go H1 pats ]
  | spec_patterns.SPureGoal ?d :: ?pats =>
      notypeclasses refine (coq_tactics.tac_specialize_assert_pure _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
       [ env_reflexivity || fail "iSpecialize:" H1 "not found"
       | solve_to_wand H1
       | iSolveTC ||
           (let Q := match goal with
                     | |- FromPure _ ?Q _ => Q
                     end in
            fail "iSpecialize:" Q "not pure")
       | env_reflexivity
       | solve_done d
       | go H1 pats ]
  | spec_patterns.SGoal
      {|
      spec_patterns.spec_goal_kind := spec_patterns.GPersistent;
      spec_patterns.spec_goal_negate := false;
      spec_patterns.spec_goal_frame := ?Hs_frame;
      spec_patterns.spec_goal_hyps := [];
      spec_patterns.spec_goal_done := ?d |} :: ?pats =>
      notypeclasses refine
       (coq_tactics.tac_specialize_assert_persistent _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
       [ env_reflexivity || fail "iSpecialize:" H1 "not found"
       | solve_to_wand H1
       | iSolveTC ||
           (let Q := match goal with
                     | |- Persistent ?Q => Q
                     end in
            fail "iSpecialize:" Q "not persistent")
       | iSolveTC
       | env_reflexivity
       | iFrame Hs_frame; solve_done d
       | go H1 pats ]
  | spec_patterns.SGoal
      {|
      spec_patterns.spec_goal_kind := spec_patterns.GPersistent;
      spec_patterns.spec_goal_negate := _;
      spec_patterns.spec_goal_frame := _;
      spec_patterns.spec_goal_hyps := _;
      spec_patterns.spec_goal_done := _ |} :: ?pats =>
      fail "iSpecialize: cannot select hypotheses for persistent premise"
  | spec_patterns.SGoal
      {|
      spec_patterns.spec_goal_kind := ?m;
      spec_patterns.spec_goal_negate := ?lr;
      spec_patterns.spec_goal_frame := ?Hs_frame;
      spec_patterns.spec_goal_hyps := ?Hs;
      spec_patterns.spec_goal_done := ?d |} :: ?pats =>
      let Hs' := eval compute in (if lr then Hs else Hs_frame ++ Hs) in
      notypeclasses refine
       (coq_tactics.tac_specialize_assert _ _ _ _ H1 _ lr Hs' _ _ _ _ _ _ _ _ _ _ _);
       [ env_reflexivity || fail "iSpecialize:" H1 "not found"
       | solve_to_wand H1
       | lazymatch m with
         | spec_patterns.GSpatial => notypeclasses refine (add_modal_id _ _)
         | spec_patterns.GModal => iSolveTC || fail "iSpecialize: goal not a modality"
         end
       | env_reflexivity ||
           (let Hs' := iMissingHyps Hs' in
            fail "iSpecialize: hypotheses" Hs' "not found")
       | iFrame Hs_frame; solve_done d
       | go H1 pats ]
  | spec_patterns.SAutoFrame spec_patterns.GPersistent :: ?pats =>
      notypeclasses refine
       (coq_tactics.tac_specialize_assert_persistent _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
       [ env_reflexivity || fail "iSpecialize:" H1 "not found"
       | solve_to_wand H1
       | iSolveTC ||
           (let Q := match goal with
                     | |- Persistent ?Q => Q
                     end in
            fail "iSpecialize:" Q "not persistent")
       | env_reflexivity
       | solve
       [ iFrame "∗ #" ]
       | go H1 pats ]
  | spec_patterns.SAutoFrame ?m :: ?pats =>
      notypeclasses refine (coq_tactics.tac_specialize_frame _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
       [ env_reflexivity || fail "iSpecialize:" H1 "not found"
       | solve_to_wand H1
       | lazymatch m with
         | spec_patterns.GSpatial => notypeclasses refine (add_modal_id _ _)
         | spec_patterns.GModal => iSolveTC || fail "iSpecialize: goal not a modality"
         end
       | first
       [ notypeclasses
       refine
       (coq_tactics.tac_unlock_emp _ _ _)
       | notypeclasses
       refine
       (coq_tactics.tac_unlock_True _ _ _)
       | iFrame "∗ #"; notypeclasses refine (coq_tactics.tac_unlock _ _ _)
       | fail "iSpecialize: premise cannot be solved by framing" ]
       | exact
       eq_refl ]; iIntro H1; go H1 pats
  end), last call failed.
Tactic failure: iSpecialize: cannot instantiate (∀ _ : φ, P -∗ False)%I with P.

These traces might be useful when developing tactics, but they are certainly not useful for our users. I wouldn't even mind the short list of nested tactics very much, but literally printing the source of locally bound Ltac functions is excessive. I think per default it should not print those bound functions, so the error would become

The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)", "iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializePat (open_constr) (constr)" and "go", last call failed.
Tactic failure: iSpecialize: cannot instantiate (∀ _ : φ, P -∗ False)%I with P.

There's still some stuff in there that users won't understand, but a least the actual error is not burried below two screen heights of dumped tactic source code.

If you are not willing to make this the default, I would appreciate at least having it available as an option.

(I somehow expected this to already be reported but couldn't find an existing report, so here you go.)

@JasonGross

This comment has been minimized.

Copy link
Contributor

commented Jun 11, 2018

I have no strong preference about the defaults, but I strongly prefer that the current mode at least be available as an option.

@ppedrot

This comment has been minimized.

Copy link
Member

commented Jun 25, 2018

Completely disabling Ltac traces would probably also help for performance, see e.g. #7385.

ppedrot added a commit to ppedrot/coq that referenced this issue Jun 28, 2018
Add an option not to register Ltac backtraces.
Fixes coq#7769: Better control over ltac backtraces.
Fixes coq#7385: Tactic allocates gigabytes of RAM.

For the lulz I disabled the option by default, let's see if that makes
any performance difference.
@robbertkrebbers

This comment has been minimized.

Copy link
Contributor

commented Nov 29, 2018

I would be strongly in favor of having an option to disable backtraces. Probably a global like Set/Unset Ltac Backtraces would do.

Arguably, by default it should be disabled, and one should only enable it manually when debugging tactics, but I care more about having such an option at all, than the default.

ppedrot added a commit to ppedrot/coq that referenced this issue Dec 5, 2018
Add an option not to register Ltac backtraces.
Fixes coq#7769: Better control over ltac backtraces.
Fixes coq#7385: Tactic allocates gigabytes of RAM.

For the lulz I disabled the option by default, let's see if that makes
any performance difference.
ppedrot added a commit to ppedrot/coq that referenced this issue Dec 5, 2018
Add an option not to register Ltac backtraces.
Fixes coq#7769: Better control over ltac backtraces.
Fixes coq#7385: Tactic allocates gigabytes of RAM.
ppedrot added a commit to ppedrot/coq that referenced this issue Dec 18, 2018
Add an option not to register Ltac backtraces.
Fixes coq#7769: Better control over ltac backtraces.
Fixes coq#7385: Tactic allocates gigabytes of RAM.
ppedrot added a commit to ppedrot/coq that referenced this issue Dec 18, 2018
Add an option not to register Ltac backtraces.
Fixes coq#7769: Better control over ltac backtraces.
Fixes coq#7385: Tactic allocates gigabytes of RAM.
ppedrot added a commit to ppedrot/coq that referenced this issue Feb 5, 2019
Add an option not to register Ltac backtraces.
Fixes coq#7769: Better control over ltac backtraces.
Fixes coq#7385: Tactic allocates gigabytes of RAM.

@Zimmi48 Zimmi48 added this to the 8.10+beta1 milestone Apr 26, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
5 participants
You can’t perform that action at this time.