search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
630 stars 142 forks source link

Holmake hangs #1353

Open xrchz opened 6 hours ago

xrchz commented 6 hours ago

At current master (i.e. 01016dcf0e02558d270fce008fce672df8cdbbf7)

Running Holmake in a directory containing only the file bugScript.sml with the following contents

open HolKernel boolLib bossLib

val _ = new_theory"bug";

Definition bug_def:
  bug = nothing to see here
Termination
  cheat
QED

val _ = export_theory();

seems to go into an infinite loop.

mn200 commented 6 hours ago

Thanks for the bug report!

mn200 commented 5 hours ago

@digama0 might be best placed to fix this.