chore(*): disable big chunk of the standard library and tests

library/.project

@@ -1,3 +1,38 @@
 + *.lean
 - flycheck*.lean
-- .#*.lean
+- .#*.lean
+- theories/
+- bag.lean
+- bv.lean
+- complex.lean
+- countable.lean
+- encodable.lean
+- equiv.lean
+- data/finset/
+- data/fintype/
+- data/int/
+- data/rat/
+- data/real/
+- data/examples/
+- algebra/category/
+- logic/examples/
+- matrix.lean
+- squash.lean
+- stream.lean
+- string.lean
+- uprod.lean
+- tuple.lean
+- fin.lean
+- pnat.lean
+- hf.lean
+- data/vector/
+- data/set/
+- interval.lean
+- group_power.lean
+- ring_power.lean
+- group_bigops.lean
+- order_bigops.lean
+- ring_bigops.lean
+- galois_connection.lean
+- complete_lattice.lean
+- homomorphism.lean

library/data/default.lean

@@ -3,6 +3,8 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jeremy Avigad
 -/
-import .empty .unit .bool .num .string .nat .int .rat .fintype
-import .prod .sum .sigma .option .list .finset .set .stream
-import .fin .real .complex
+
+import .empty .unit .bool .num .nat .list
+--  .set
+-- import .string .int .rat .fintype .prod .sum .sigma .option .list .finset .set .stream
+-- import .fin .real .complex

library/data/list/comb.lean

@@ -5,7 +5,8 @@ Authors: Leonardo de Moura, Haitao Zhang, Floris van Doorn
 
 List combinators.
 -/
-import data.list.basic data.equiv
+-- TODO(Leo): uncomment data.equiv after refactoring
+import data.list.basic -- data.equiv
 open nat prod decidable function helper_tactics
 
 namespace list
@@ -567,6 +568,7 @@ not.mto (mem_of_dinj_of_mem_dmap Pdi Pa)
 
 end dmap
 
+/-
 section
 open equiv
 definition list_equiv_of_equiv {A B : Type} : A ≃ B → list A ≃ list B
@@ -618,6 +620,8 @@ suppose A ≃ nat, calc
      ... ≃ nat      : list_nat_equiv_nat
      ... ≃ A        : this
 end
+-/
+
 end list
 
 attribute list.decidable_any [instance]

library/data/nat/bigops.lean

@@ -5,6 +5,8 @@ Author: Jeremy Avigad
 
 Finite sums and products over intervals of natural numbers.
 -/
+-- TODO(Leo): remove after refactoring
+exit
 import data.nat.order algebra.group_bigops algebra.interval
 
 namespace nat

library/data/nat/parity.lean

@@ -5,6 +5,8 @@ Authors: Leonardo de Moura
 
 Parity.
 -/
+-- TODO(Leo): remove after refactoring
+exit
 import data.nat.power logic.identities
 
 namespace nat

library/data/nat/power.lean

@@ -5,6 +5,10 @@ Authors: Leonardo de Moura, Jeremy Avigad
 
 The power function on the natural numbers.
 -/
+
+-- TODO(Leo): remove after refactoring
+exit
+
 import data.nat.basic data.nat.order data.nat.div data.nat.gcd algebra.ring_power
 
 namespace nat

src/shell/CMakeLists.txt

@@ -53,9 +53,9 @@ add_test(NAME "show_goal"
 add_test(NAME "show_goal_bag"
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
          COMMAND bash "./show_goal_bag.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
-add_test(NAME "print_info"
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
-         COMMAND bash "./print_info.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
+# add_test(NAME "print_info"
+#          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
+#          COMMAND bash "./print_info.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
 add_test(NAME "dir_option"
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
          COMMAND "${LEAN_SOURCE_DIR}/../bin/lean" "--dir=${LEAN_SOURCE_DIR}/../library/data/nat" "dir_option.lean")
@@ -133,14 +133,14 @@ FOREACH(T ${LEANSLOWTESTS})
   set_tests_properties("leanslowtest_${T_NAME}" PROPERTIES LABELS "expensive")
 ENDFOREACH(T)
 
-# LEAN DOCS
-file(GLOB LEANDOCS "${LEAN_SOURCE_DIR}/../doc/lean/*.org")
-FOREACH(T ${LEANDOCS})
-  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
-  add_test(NAME "leandoc_${T_NAME}"
-           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/lean"
-           COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
-ENDFOREACH(T)
+# # LEAN DOCS
+# file(GLOB LEANDOCS "${LEAN_SOURCE_DIR}/../doc/lean/*.org")
+# FOREACH(T ${LEANDOCS})
+#   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+#   add_test(NAME "leandoc_${T_NAME}"
+#            WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/lean"
+#            COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
+# ENDFOREACH(T)
 
 # # Create the script lean.sh
 # # This is used to create a soft dependency on the Lean executable

src/tests/shell/file1.lean

@@ -1,6 +1,6 @@
 check nat
 check nat.add_zero
 check nat.zero_add
-check finset
+-- check finset
 inductive foo : Type :=
 mk : foo → foo

src/tests/shell/file2.lean

@@ -1,7 +1,7 @@
 check nat
 check nat.add_zero
 check nat.zero_add
-check finset
+-- check finset
 
 open nat
 example (a b : nat) : a = 0 → b = 0 → a = b :=

tests/lean/interactive/coe.input

@@ -1,3 +0,0 @@
-VISIT coe.lean
-WAIT
-INFO 5 16

tests/lean/interactive/coe.input.expected.out

@@ -1,13 +0,0 @@
--- BEGINWAIT
--- ENDWAIT
--- BEGININFO
--- TYPE|5|16
-decidable (a = b)
--- ACK
--- SYNTH|5|16
-has_decidable_eq a b
--- ACK
--- SYMBOL|5|16
-_
--- ACK
--- ENDINFO

tests/lean/interactive/coe.lean

@@ -1,9 +0,0 @@
-import data.int
-open int
-
-protected theorem has_decidable_eq₁ [instance] : decidable_eq ℤ :=
-take (a b : ℤ), _
-
-constant n : nat
-constant i : int
-check n + i

tests/lean/run/coe10.lean

@@ -1,17 +0,0 @@
-import data.nat
-open nat
-
-inductive fn2 (A B C : Type) :=
-mk : (A → C) → (B → C) → fn2 A B C
-
-definition to_ac [coercion] {A B C : Type} (f : fn2 A B C) : A → C :=
-fn2.rec (λ f g, f) f
-
-definition to_bc [coercion] {A B C : Type} (f : fn2 A B C) : B → C :=
-fn2.rec (λ f g, g) f
-
-constant f : fn2 Prop nat nat
-constant a : Prop
-constant n : nat
-check f a
-check f n