max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(shell/lean): error if leandoc is used with smt2 files

Browse source
This commit is contained in:
Leonardo de Moura 2016-11-27 19:43:26 -08:00
parent fcef94200f
commit 5fe0068301
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/shell/lean.cpp
View file

@ -368,6 +368,7 @@ int main(int argc, char ** argv) {
#endif
environment env = mk_environment(trust_lvl);
io_state ios(opts, lean::mk_pretty_formatter_factory());
#if defined(LEAN_SERVER)
if (json_output) {
@ -382,6 +383,7 @@ int main(int argc, char ** argv) {
bool ok = true;
for (int i = optind; i < argc; i++) {
try {
if (doc) throw lean::exception("leandoc does not support .smt2 files");
ok = ::lean::smt2::parse_commands(env, ios, argv[i]);
} catch (lean::exception & ex) {
ok = false;