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

quiet load #1336

Closed digama0 closed 1 week ago

digama0 commented 2 weeks ago

This implements a flag quiet_load which makes load not print to stdErr (but it still throws errors). The qload function is shorthand for running load with quiet_load set to true. This is intended for IDEs that want to preload the opens of a file without getting errors for nonexistent or already open modules.

mn200 commented 1 week ago

Please undo reversion of theory changes.

digama0 commented 1 week ago

Master is still broken. I will rebase on top of #1338 instead?

mn200 commented 1 week ago

Thanks for this cleanup!