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

HOL/tools/check-builds does not call systeml polyc. #1334

Closed ordinarymath closed 2 weeks ago

ordinarymath commented 2 weeks ago

checkbuilds seems to directly call polyc from system env which is an issue for cases where i dont have polyc in my path. a workaround is commenting out the line in tools/sequences/kernel or temporarily adding polyc into system path

mn200 commented 2 weeks ago

Thanks for this; the Holmakefile should be using $(POLYC).