From 774fa01b1a60ac9b91bd6e2262fec7ab3d8572ed Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Feb 2016 14:55:21 -0800 Subject: [PATCH] chore(library/pp_options): reduce pp default limits --- src/library/pp_options.cpp | 4 +- tests/lean/955.lean | 286 +++++++++++++++++++++++++++++++ tests/lean/955.lean.expected.out | 2 + 3 files changed, 290 insertions(+), 2 deletions(-) create mode 100644 tests/lean/955.lean create mode 100644 tests/lean/955.lean.expected.out diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp index be0a11a25..91f40b12a 100644 --- a/src/library/pp_options.cpp +++ b/src/library/pp_options.cpp @@ -8,11 +8,11 @@ Author: Leonardo de Moura #include "library/pp_options.h" #ifndef LEAN_DEFAULT_PP_MAX_DEPTH -#define LEAN_DEFAULT_PP_MAX_DEPTH 10000 +#define LEAN_DEFAULT_PP_MAX_DEPTH 64 #endif #ifndef LEAN_DEFAULT_PP_MAX_STEPS -#define LEAN_DEFAULT_PP_MAX_STEPS 50000 +#define LEAN_DEFAULT_PP_MAX_STEPS 5000 #endif #ifndef LEAN_DEFAULT_PP_NOTATION diff --git a/tests/lean/955.lean b/tests/lean/955.lean new file mode 100644 index 000000000..a4169f7bc --- /dev/null +++ b/tests/lean/955.lean @@ -0,0 +1,286 @@ +-*- mode: compilation; default-directory: "~/projects/lean/tests/lean/run/" -*- +Compilation started at Thu Feb 4 14:53:07 + +/home/leo/projects/lean/bin/lean -Dpp.width=120 /home/leo/projects/lean/tests/lean/run/955.lean +/home/leo/projects/lean/tests/lean/run/955.lean:31:32: error: type mismatch at definition 'append_auxH', has type + @vectorH.{?M_1} + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (… + …)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + ?M_4 +but is expected to have type + @vectorH.{?M_1} + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (… + …)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + (@vector.append_aux.{?M_1+1} Type.{?M_1} nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (nat.addl + nat.zero + (… + …)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + (@vector.nil.{?M_1+1} Type.{?M_1}) + ?M_3) +The following identifier(s) are introduced as free variables by the left-hand-side of the equation: + v' + +Compilation exited abnormally with code 1 at Thu Feb 4 14:53:09 diff --git a/tests/lean/955.lean.expected.out b/tests/lean/955.lean.expected.out new file mode 100644 index 000000000..a7e1d1462 --- /dev/null +++ b/tests/lean/955.lean.expected.out @@ -0,0 +1,2 @@ +955.lean:1:1: error: unexpected token +955.lean: error: 955.lean:1:21: error: unexpected token