z

leanprover · Feb 8, 2025 · b16dae1 · b16dae1
1 parent 620775a
commit b16dae1
Show file tree

Hide file tree

Showing 48 changed files with 3 additions and 9 deletions.
diff --git a/Lean/Export.lean → Export.lean b/Lean/Export.lean → Export.lean
diff --git a/Lean/KLR.lean → KLR.lean b/Lean/KLR.lean → KLR.lean
diff --git a/Lean/KLR/Core.lean → KLR/Core.lean b/Lean/KLR/Core.lean → KLR/Core.lean
diff --git a/Lean/KLR/Core/Basic.lean → KLR/Core/Basic.lean b/Lean/KLR/Core/Basic.lean → KLR/Core/Basic.lean
diff --git a/Lean/KLR/Core/Encode.lean → KLR/Core/Encode.lean b/Lean/KLR/Core/Encode.lean → KLR/Core/Encode.lean
diff --git a/Lean/KLR/Core/Oper.lean → KLR/Core/Oper.lean b/Lean/KLR/Core/Oper.lean → KLR/Core/Oper.lean
diff --git a/Lean/KLR/Core/Pretty.lean → KLR/Core/Pretty.lean b/Lean/KLR/Core/Pretty.lean → KLR/Core/Pretty.lean
diff --git a/Lean/KLR/Python.lean → KLR/Python.lean b/Lean/KLR/Python.lean → KLR/Python.lean
diff --git a/Lean/KLR/Trace.lean → KLR/Trace.lean b/Lean/KLR/Trace.lean → KLR/Trace.lean
diff --git a/Lean/KLR/Trace/Basic.lean → KLR/Trace/Basic.lean b/Lean/KLR/Trace/Basic.lean → KLR/Trace/Basic.lean
diff --git a/Lean/KLR/Trace/Builtin.lean → KLR/Trace/Builtin.lean b/Lean/KLR/Trace/Builtin.lean → KLR/Trace/Builtin.lean
diff --git a/Lean/KLR/Trace/NKI.lean → KLR/Trace/NKI.lean b/Lean/KLR/Trace/NKI.lean → KLR/Trace/NKI.lean
diff --git a/Lean/KLR/Trace/Python.lean → KLR/Trace/Python.lean b/Lean/KLR/Trace/Python.lean → KLR/Trace/Python.lean
diff --git a/Lean/KLR/Trace/Tensor.lean → KLR/Trace/Tensor.lean b/Lean/KLR/Trace/Tensor.lean → KLR/Trace/Tensor.lean
diff --git a/Lean/KLR/Trace/Types.lean → KLR/Trace/Types.lean b/Lean/KLR/Trace/Types.lean → KLR/Trace/Types.lean
diff --git a/Lean/KLR/Util.lean → KLR/Util.lean b/Lean/KLR/Util.lean → KLR/Util.lean
diff --git a/Lean/Main.lean → Main.lean b/Lean/Main.lean → Main.lean
diff --git a/bin/klr b/bin/klr
@@ -2,4 +2,4 @@
 
 ROOT=$(dirname $(dirname $(readlink -f $0)))
 
-$ROOT/Lean/.lake/build/bin/klr $@
+$ROOT/.lake/build/bin/klr $@
diff --git a/bin/make-wheel b/bin/make-wheel
@@ -4,19 +4,13 @@ trap "kill 0" SIGINT SIGTERM
 
 ROOT=$(dirname $(dirname $(readlink -f $0)))
 WHEEL_DIR=$ROOT/.wheel/
-LEAN_DIR=$ROOT/Lean
-PYTHON_DIR=$ROOT/Python
+PYTHON_DIR=$ROOT/interop
 rm -rf $WHEEL_DIR
 mkdir -p $WHEEL_DIR/{klr,bin}
-
-# Build Lean code
-pushd .
-cd $LEAN_DIR
 lake build
-popd
 
 # Get klr binary
-cp $LEAN_DIR/.lake/build/bin/klr $WHEEL_DIR/bin/klr
+cp .lake/build/bin/klr $WHEEL_DIR/bin/klr
 
 # Get Python packages
 cp -R $PYTHON_DIR/* $WHEEL_DIR

diff --git a/Python/MANIFEST.in → interop/MANIFEST.in b/Python/MANIFEST.in → interop/MANIFEST.in
diff --git a/Python/README.md → interop/README.md b/Python/README.md → interop/README.md
diff --git a/Python/klr/__init__.py → interop/klr/__init__.py b/Python/klr/__init__.py → interop/klr/__init__.py
diff --git a/Python/klr/parser.py → interop/klr/parser.py b/Python/klr/parser.py → interop/klr/parser.py
diff --git a/Python/nki/__init__.py → interop/nki/__init__.py b/Python/nki/__init__.py → interop/nki/__init__.py
diff --git a/Python/nki/isa/__init__.py → interop/nki/isa/__init__.py b/Python/nki/isa/__init__.py → interop/nki/isa/__init__.py
diff --git a/Python/nki/language/__init__.py → interop/nki/language/__init__.py b/Python/nki/language/__init__.py → interop/nki/language/__init__.py
diff --git a/Python/noop.c → interop/noop.c b/Python/noop.c → interop/noop.c
diff --git a/Python/pyproject.toml → interop/pyproject.toml b/Python/pyproject.toml → interop/pyproject.toml
diff --git a/Python/requirements.txt → interop/requirements.txt b/Python/requirements.txt → interop/requirements.txt
diff --git a/Python/tests/examples/__init__.py → interop/tests/examples/__init__.py b/Python/tests/examples/__init__.py → interop/tests/examples/__init__.py
diff --git a/Python/tests/examples/average_pool.py → interop/tests/examples/average_pool.py b/Python/tests/examples/average_pool.py → interop/tests/examples/average_pool.py
diff --git a/Python/tests/examples/fused_mamba.py → interop/tests/examples/fused_mamba.py b/Python/tests/examples/fused_mamba.py → interop/tests/examples/fused_mamba.py
diff --git a/Python/tests/examples/getting_started.py → interop/tests/examples/getting_started.py b/Python/tests/examples/getting_started.py → interop/tests/examples/getting_started.py
diff --git a/Python/tests/examples/index.py → interop/tests/examples/index.py b/Python/tests/examples/index.py → interop/tests/examples/index.py
diff --git a/Python/tests/examples/layernorm.py → interop/tests/examples/layernorm.py b/Python/tests/examples/layernorm.py → interop/tests/examples/layernorm.py
diff --git a/Python/tests/examples/layout.py → interop/tests/examples/layout.py b/Python/tests/examples/layout.py → interop/tests/examples/layout.py
diff --git a/Python/tests/examples/matmul.py → interop/tests/examples/matmul.py b/Python/tests/examples/matmul.py → interop/tests/examples/matmul.py
diff --git a/Python/tests/examples/mm.py → interop/tests/examples/mm.py b/Python/tests/examples/mm.py → interop/tests/examples/mm.py
diff --git a/Python/tests/examples/prof.py → interop/tests/examples/prof.py b/Python/tests/examples/prof.py → interop/tests/examples/prof.py
diff --git a/Python/tests/examples/rmsnorm.py → interop/tests/examples/rmsnorm.py b/Python/tests/examples/rmsnorm.py → interop/tests/examples/rmsnorm.py
diff --git a/Python/tests/examples/sd_attention.py → interop/tests/examples/sd_attention.py b/Python/tests/examples/sd_attention.py → interop/tests/examples/sd_attention.py
diff --git a/Python/tests/examples/tensor_addition.py → interop/tests/examples/tensor_addition.py b/Python/tests/examples/tensor_addition.py → interop/tests/examples/tensor_addition.py
diff --git a/Python/tests/examples/transpose2d.py → interop/tests/examples/transpose2d.py b/Python/tests/examples/transpose2d.py → interop/tests/examples/transpose2d.py
diff --git a/Python/tests/test_basic.py → interop/tests/test_basic.py b/Python/tests/test_basic.py → interop/tests/test_basic.py
diff --git a/Python/tests/test_examples.py → interop/tests/test_examples.py b/Python/tests/test_examples.py → interop/tests/test_examples.py
diff --git a/Lean/lake-manifest.json → lake-manifest.json b/Lean/lake-manifest.json → lake-manifest.json
diff --git a/Lean/lakefile.lean → lakefile.lean b/Lean/lakefile.lean → lakefile.lean
diff --git a/Lean/lean-toolchain → lean-toolchain b/Lean/lean-toolchain → lean-toolchain
Original file line number	Diff line number	Diff line change
Expand Up		@@ -2,4 +2,4 @@

		ROOT=$(dirname $(dirname $(readlink -f $0)))

		$ROOT/Lean/.lake/build/bin/klr $@
		$ROOT/.lake/build/bin/klr $@