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

Warn if modules / theories only differ by case #679

Open mn200 opened 5 years ago

mn200 commented 5 years ago

This leads to very strange errors on case-insensitive file systems. Also arises if a theory is referenced in one place with one capitalisation and in another with a different one.

mn200 commented 5 years ago

Better yet (perhaps?): detect if FS is case-insensitive, record this fact, and then change operations like load to normalise filenames before using then.