stevemessick
commented
5 days ago @realharryhero I don't understand your code. What language is it written in? What errors are you seeing?
Open realharryhero opened 1 week ago
stevemessick
commented
5 days ago @realharryhero I don't understand your code. What language is it written in? What errors are you seeing?
Hello! For a competition, I want to use tools that are far outside those that are normally used, say for the most recent math-like competition, including LEAN and many scripts. But for example, trying to use LEAN on the kaggle notebook with this code causes some errors:
Code
```lean cd /kaggle/working sudo apt-get update set -exo pipefail sudo apt-get install -y --install-suggests git libgmp-dev cmake ccache clang bash -c 'curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:v4.7.0 || (echo && read -n 1 -s -r -p "Install failed, press ENTER to continue...")' source ~/.profile elan self update lake_do () { lake update lake build } lake new my_project cd my_project lake update lake build echo 'got here' printf '\nrequire mathlib from /kaggle/working/mathlib4' >> ./lakefile.lean printf 'leanprover/lean4:v4.7.0' > ./lean-toolchain cat ./lakefile.lean lake update lake build printf '\n\nimport Mathlib.Topology.Basic\n\n#check TopologicalSpace' >> ./Main.lean lake update lake build lake env lean --run ./Main.lean ```
Various other (seemingly unrelated) issues pop up with other tools I'd like to use, and I believe this is due to the extremely large amount of packages uploaded in each kaggle notebook that would normally be used for commonly-used ML packages like torch or tensorflow, etc. Is there a way to reboot a kaggle notebook into a sort-of "minimal instance" without so many packages? Thank you!