search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
491 stars 88 forks source link

proofdepth sometimes ends up being nil #8

Open cpitclaudel opened 9 years ago

cpitclaudel commented 9 years ago

From time to time I get this message:

Debugger entered--Lisp error: (wrong-type-argument number-or-marker-p nil)
  =(nil 0)
  (if (= proofdepth 0) (proof-clean-buffer proof-goals-buffer))
  (let* (ans (naborts 0) (nundos 0) (proofdepth (coq-get-span-proofnum span)) (proofstack (coq-get-span-proofstack span)) (span-staten (coq-get-span-statenum span)) (naborts (count-not-intersection coq-last-but-one-proofstack proofstack))) (if (= proofdepth 0) (proof-clean-buffer proof-goals-buffer)) (if (and (equal coq-last-but-one-proofstack proofstack) (= coq-last-but-one-proofnum proofdepth) (= coq-last-but-one-statenum span-staten)) nil (list (format "Backtrack %s %s %s . " (int-to-string span-staten) (int-to-string proofdepth) naborts))))
  (if (eq (span-property span (quote type)) (quote proverproc)) nil (let* (ans (naborts 0) (nundos 0) (proofdepth (coq-get-span-proofnum span)) (proofstack (coq-get-span-proofstack span)) (span-staten (coq-get-span-statenum span)) (naborts (count-not-intersection coq-last-but-one-proofstack proofstack))) (if (= proofdepth 0) (proof-clean-buffer proof-goals-buffer)) (if (and (equal coq-last-but-one-proofstack proofstack) (= coq-last-but-one-proofnum proofdepth) (= coq-last-but-one-statenum span-staten)) nil (list (format "Backtrack %s %s %s . " (int-to-string span-staten) (int-to-string proofdepth) naborts)))))
  coq-find-and-forget(#<overlay from 32260 to 32313 in ADTExamples.v>)
  funcall(coq-find-and-forget #<overlay from 32260 to 32313 in ADTExamples.v>)
  (proof-setup-retract-action start end (funcall proof-find-and-forget-fn target) undo-action displayflags)
  (nconc actions (proof-setup-retract-action start end (funcall proof-find-and-forget-fn target) undo-action displayflags))
  (setq actions (nconc actions (proof-setup-retract-action start end (funcall proof-find-and-forget-fn target) undo-action displayflags)))
  (if (> end start) (setq actions (nconc actions (proof-setup-retract-action start end (funcall proof-find-and-forget-fn target) undo-action displayflags))))
  (let ((end (proof-unprocessed-begin)) (start (span-start target)) (span (if proof-arbitrary-undo-positions target (proof-last-goal-or-goalsave))) actions) (if (and span proof-kill-goal-command (not (or (memq (span-property span (quote type)) (quote (goalsave proverproc)))))) (if (< (span-end span) (span-end target)) (progn (setq span target) (while (and span (memq (span-property span ...) (quote ...))) (setq span (next-span span (quote type)))) (setq actions (proof-setup-retract-action start end (if (null span) nil (funcall proof-count-undos-fn span)) undo-action) end start)) (setq proof-nesting-depth (1- proof-nesting-depth)) (setq actions (proof-setup-retract-action (span-start span) end (list proof-kill-goal-command) undo-action displayflags) end (span-start span)))) (if (> end start) (setq actions (nconc actions (proof-setup-retract-action start end (funcall proof-find-and-forget-fn target) undo-action displayflags)))) (proof-start-queue (min start end) (proof-unprocessed-begin) actions (quote retracting)))
  proof-retract-target(#<overlay from 32260 to 32313 in ADTExamples.v> nil nil)
  (if span (proof-retract-target span undo-action displayflags) (proof-debug "proof-retract-until-point: couldn't find a span!"))
  (let ((span (span-at (point) (quote type)))) (if span nil (proof-goto-end-of-locked) (backward-char) (setq span (span-at (point) (quote type)))) (if span (proof-retract-target span undo-action displayflags) (proof-debug "proof-retract-until-point: couldn't find a span!")))
  (if (proof-locked-region-empty-p) nil (let ((span (span-at (point) (quote type)))) (if span nil (proof-goto-end-of-locked) (backward-char) (setq span (span-at (point) (quote type)))) (if span (proof-retract-target span undo-action displayflags) (proof-debug "proof-retract-until-point: couldn't find a span!"))))
  (if (proof-locked-region-empty-p) (error "No locked region") (proof-activate-scripting) (proof-shell-ready-prover) (if (proof-locked-region-empty-p) nil (let ((span (span-at (point) (quote type)))) (if span nil (proof-goto-end-of-locked) (backward-char) (setq span (span-at (point) (quote type)))) (if span (proof-retract-target span undo-action displayflags) (proof-debug "proof-retract-until-point: couldn't find a span!")))))
  proof-retract-until-point(nil)
  (progn (goto-char (span-start lastspan)) (proof-retract-until-point undo-action))
  (if (setq lastspan (span-at-before (proof-unprocessed-begin) (quote type))) (progn (goto-char (span-start lastspan)) (proof-retract-until-point undo-action)) (error "Nothing to undo!"))
  (if (proof-locked-region-empty-p) nil (if (setq lastspan (span-at-before (proof-unprocessed-begin) (quote type))) (progn (goto-char (span-start lastspan)) (proof-retract-until-point undo-action)) (error "Nothing to undo!")))
  (save-excursion (if (proof-locked-region-empty-p) nil (if (setq lastspan (span-at-before (proof-unprocessed-begin) (quote type))) (progn (goto-char (span-start lastspan)) (proof-retract-until-point undo-action)) (error "Nothing to undo!"))))
  (let (lastspan) (save-excursion (if (proof-locked-region-empty-p) nil (if (setq lastspan (span-at-before (proof-unprocessed-begin) (quote type))) (progn (goto-char (span-start lastspan)) (proof-retract-until-point undo-action)) (error "Nothing to undo!")))) (if lastspan (proof-maybe-follow-locked-end (span-start lastspan))))
  (progn (let (lastspan) (save-excursion (if (proof-locked-region-empty-p) nil (if (setq lastspan (span-at-before (proof-unprocessed-begin) (quote type))) (progn (goto-char (span-start lastspan)) (proof-retract-until-point undo-action)) (error "Nothing to undo!")))) (if lastspan (proof-maybe-follow-locked-end (span-start lastspan)))))
  (cond ((eq proof-buffer-type (quote script)) (progn (let (lastspan) (save-excursion (if (proof-locked-region-empty-p) nil (if (setq lastspan ...) (progn ... ...) (error "Nothing to undo!")))) (if lastspan (proof-maybe-follow-locked-end (span-start lastspan)))))) ((buffer-live-p proof-script-buffer) (save-current-buffer (set-buffer proof-script-buffer) (let (lastspan) (save-excursion (if (proof-locked-region-empty-p) nil (if (setq lastspan ...) (progn ... ...) (error "Nothing to undo!")))) (if lastspan (proof-maybe-follow-locked-end (span-start lastspan)))))))
  proof-undo-last-successful-command-1()
  proof-undo-last-successful-command()
  funcall-interactively(proof-undo-last-successful-command)
  #<subr call-interactively>(proof-undo-last-successful-command nil nil)
  ad-Advice-call-interactively(#<subr call-interactively> proof-undo-last-successful-command nil nil)
  apply(ad-Advice-call-interactively #<subr call-interactively> (proof-undo-last-successful-command nil nil))
  call-interactively(proof-undo-last-successful-command nil nil)
  command-execute(proof-undo-last-successful-command)

I don't have a good way to reproduce this yet, unfortunately.

Matafou commented 9 years ago

I see this also from time to time, no idea why.

proofdepth is stored in spans after each command is issued. There must be some strange cases where the information is not stored in the span, leading to this error.

I just added a warning in an early place where I suspect we would better understand the problem. Wait and see.

cpitclaudel commented 8 years ago

Could it be cases where processing is cancelled (C-g) before these tags are added? Are they maybe added too late?