michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(bin/linja): add --discard and --to_axiom options

Browse source
This commit is contained in:
Soonho Kong 2014-10-14 18:56:17 -07:00
parent e6606ef2ac
commit c92260d9ec
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
bin/linja
View file

@ -244,6 +244,10 @@ def get_lean_options(args):
args.lean_options = []
if args.flycheck:
args.lean_options.append("--flycheck")
if args.discard:
args.lean_options.append("--discard")
if args.to_axiom:
args.lean_options.append("--to_axiom")
if args.cache:
args.lean_options += ["-c", args.cache]
if args.lean_config_option:
@ -260,6 +264,8 @@ def parse_arg(argv):
parser.add_argument('--lean-config-option', '-D', action='append', help="set a Lean configuration option (name=value)")
parser.add_argument('--verbose', '-v', action='store_true', help="turn on verbose option")
parser.add_argument('--keep-going', '-k', action='store', default=None, const=1, nargs='?', help="keep going until N jobs fail [default=1]")
parser.add_argument('--discard', '-T', action='store_true', default=False, help="discard the proof of imported theorems after checking")
parser.add_argument('--to_axiom', '-X', action='store_true', default=False, help="discard proofs of all theorems after checking them, i.e., theorems become axioms after checking")
parser.add_argument('targets', nargs='*')
args = parser.parse_args(argv)
check_requirements()