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.
When determining the properties of dependencies, it would pause for 1 second after each one, making it look like more work than it actually is and also slowing down the tool. I left the 3 second countdown after all settings are confirmed, although 3 seconds is a bit short for a human to respond to the information.
mn200
commented
2 months ago
When determining the properties of dependencies, it would pause for 1 second after each one, making it look like more work than it actually is and also slowing down the tool. I left the 3 second countdown after all settings are confirmed, although 3 seconds is a bit short for a human to respond to the information.