Skip to content

Resume fails with --fast #1909

@myreen

Description

@myreen

I've noticed that Holmake --fast fails in case suspend/Resume is used. This is quite inconvenient.

Here's a simple reproduction of the error. Have a file fooScript.sml with the content:

Theory foo
Ancestors
  list

Theorem lemma:
  ∀n. n < n + 1:num
Proof
  Cases
  >- fs []
  >- suspend "bar"
QED

Resume lemma[bar]:
  simp []
QED

Finalise lemma

With Holmake fooTheory this builds fine.

With Holmake --fast fooTheory this file fails to build. The error is "No suspension with name lemma".

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions