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
621 stars 140 forks source link

hol --help #171

Open myreen opened 10 years ago

myreen commented 10 years ago

I can't seem to find any documentation about command-line arguments for hol. Holmake's command-line arguments are well documented, both in the Description and also Holmake --help.

Are there command-line arguments for hol? If there are, then there should also be support for hol --help for listing the available command-line arguments.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

mn200 commented 10 years ago

I agree there's no real documentation here. The short answer is that are no command-line arguments. This is basically because I don't know what to do to make the arguments handled uniformly across Windows and Unix.