Zulip Chat Archive
Stream: mathlib4
Topic: mathlib3port as a dependency
Alexander Bentkamp (Jan 28 2022 at 13:15):
How do I use mathbin in my project? I had it working before, but now I tried to update to a new version and it does not work any more. My lakefile looks like this:
import Lake
open Lake DSL
package test where
dependencies := #[{
name := "mathlib3port",
src := Source.git "https://github.com/leanprover-community/mathlib3port.git" "91923f396bdac71db6f87ce4ea6f5d382212fad2",
}]
defaultFacet := PackageFacet.oleans
The output of lake build is this:
% lake build
info: mathlib3port: cloning https://github.com/leanprover-community/mathlib3port.git to ./lean_packages/mathlib3port
info: lean3port: cloning https://github.com/leanprover-community/lean3port.git to ./lean_packages/lean3port
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git to ./lean_packages/mathlib
> curl -L -O https://github.com/leanprover-community/mathport/releases/download/nightly-2022-01-27/lean3-binport.tar.gz # in directory ./lean_packages/lean3port/./build/lib
> curl -L -O https://github.com/leanprover-community/mathport/releases/download/nightly-2022-01-27/lean3-synport.tar.gz # in directory ./lean_packages/lean3port/.
> curl -L -O https://github.com/leanprover-community/mathport/releases/download/nightly-2022-01-27/mathlib3-synport.tar.gz # in directory ./lean_packages/mathlib3port/.
> curl -L -O https://github.com/leanprover-community/mathport/releases/download/nightly-2022-01-27/mathlib3-binport.tar.gz # in directory ./lean_packages/mathlib3port/./build/lib
error: % Total % Received % Xferd Average Speed Time Time Time Current
Dload Upload Total Spent Left Speed
100 659 100 659 0 0 2076 0 --:--:-- --:--:-- --:--:-- 2118
100 228k 100 228k 0 0 351k 0 --:--:-- --:--:-- --:--:-- 351k
> tar -xzvf lean3-synport.tar.gz # in directory ./lean_packages/lean3port/.
error: x ./
x ./Leanbin/
x ./Leanbin/Tools/
x ./Leanbin/Tools/Debugger/
x ./Leanbin/Tools/Debugger/Util.lean
...
x ./Leanbin/System/
x ./Leanbin/System/Io.lean
x ./Leanbin/System/IoInterface.lean
x ./Leanbin/System/Random.lean
x ./Leanbin/All.lean
error: % Total % Received % Xferd Average Speed Time Time Time Current
Dload Upload Total Spent Left Speed
100 659 100 659 0 0 2140 0 --:--:-- --:--:-- --:--:-- 2189
100 5938k 100 5938k 0 0 3309k 0 0:00:01 0:00:01 --:--:-- 5227k
> tar -xzvf lean3-binport.tar.gz # in directory ./lean_packages/lean3port/./build/lib
error: x ./
x ./Leanbin/
x ./Leanbin/Tools/
x ./Leanbin/Tools/Debugger/
x ./Leanbin/Tools/Debugger/Default.olean
...
x ./Leanbin/System/
x ./Leanbin/System/Io.olean
x ./Leanbin/System/IoInterface.olean
x ./Leanbin/System/Random.olean
x ./Leanbin/All.olean
error: % Total % Received % Xferd Average Speed Time Time Time Current
Dload Upload Total Spent Left Speed
100 662 100 662 0 0 1601 0 --:--:-- --:--:-- --:--:-- 1626
100 6899k 100 6899k 0 0 2089k 0 0:00:03 0:00:03 --:--:-- 2779k
> tar -xzvf mathlib3-synport.tar.gz # in directory ./lean_packages/mathlib3port/.
error: x ./
x ./Mathbin/
x ./Mathbin/RepresentationTheory/
x ./Mathbin/RepresentationTheory/Maschke.lean
x ./Mathbin/AlgebraicTopology/
x ./Mathbin/AlgebraicTopology/SimplicialSet.lean
...
x ./Mathbin/LinearAlgebra/Projection.lean
x ./Mathbin/Testing/
x ./Mathbin/Testing/SlimCheck/
x ./Mathbin/Testing/SlimCheck/Gen.lean
x ./Mathbin/Testing/SlimCheck/Functions.lean
x ./Mathbin/Testing/SlimCheck/Sampleable.lean
x ./Mathbin/Testing/SlimCheck/Testable.lean
error: % Total % Received % Xferd Average Speed Time Time Time Current
Dload Upload Total Spent Left Speed
100 662 100 662 0 0 2058 0 --:--:-- --:--:-- --:--:-- 2088
100 493M 100 493M 0 0 6130k 0 0:01:22 0:01:22 --:--:-- 5517k
> tar -xzvf mathlib3-binport.tar.gz # in directory ./lean_packages/mathlib3port/./build/lib
error: x ./
x ./Mathbin/
x ./Mathbin/RepresentationTheory/
x ./Mathbin/RepresentationTheory/Maschke.olean
x ./Mathbin/AlgebraicTopology/
x ./Mathbin/AlgebraicTopology/AlternatingFaceMapComplex.olean
x ./Mathbin/AlgebraicTopology/MooreComplex.olean
...
x ./Mathbin/Testing/SlimCheck/
x ./Mathbin/Testing/SlimCheck/Gen.olean
x ./Mathbin/Testing/SlimCheck/Sampleable.olean
x ./Mathbin/Testing/SlimCheck/Functions.olean
x ./Mathbin/Testing/SlimCheck/Testable.olean
> LEAN_PATH=./lean_packages/mathlib3port/./build/lib:./lean_packages/mathlib/./build/lib:./lean_packages/lean3port/./build/lib:./build/lib /Users/alex/.elan/toolchains/leanprover--lean4---nightly-2022-01-27/bin/lean -R ./. -o ./build/lib/Test.olean ././Test.lean
invalid output from `/Users/alex/.elan/toolchains/leanprover--lean4---nightly-2021-10-29/bin/lake print-paths Init Mathbin.AlgebraicGeometry.Scheme`:
./lean_packages/mathlib/././Mathlib/Util/Export.lean:197:51: error: unknown identifier 'default'
stderr:
mathlib3port: trying to update ./lean_packages/mathlib3port to revision 91923f396bdac71db6f87ce4ea6f5d382212fad2
lean3port: trying to update ./lean_packages/lean3port to revision 376835ea3c4dca48066838bcb1aad5c21995b261
mathlib: trying to update ./lean_packages/mathlib to revision 23d4e91230a6ffa4ea1258c4b1b4a142bcdcd7c0
> LEAN_PATH=./lean_packages/mathlib/./build/lib /Users/alex/.elan/toolchains/leanprover--lean4---nightly-2021-10-29/bin/lean -R ./lean_packages/mathlib/./. -o ./lean_packages/mathlib/./build/lib/Mathlib/Util/TermUnsafe.olean ./lean_packages/mathlib/././Mathlib/Util/TermUnsafe.lean
> LEAN_PATH=./lean_packages/mathlib/./build/lib /Users/alex/.elan/toolchains/leanprover--lean4---nightly-2021-10-29/bin/lean -R ./lean_packages/mathlib/./. -o ./lean_packages/mathlib/./build/lib/Mathlib/Util/Export.olean ./lean_packages/mathlib/././Mathlib/Util/Export.lean
> LEAN_PATH=./lean_packages/mathlib/./build/lib /Users/alex/.elan/toolchains/leanprover--lean4---nightly-2021-10-29/bin/lean -R ./lean_packages/mathlib/./. -o ./lean_packages/mathlib/./build/lib/Mathlib/Tactic/Cache.olean ./lean_packages/mathlib/././Mathlib/Tactic/Cache.lean
But when I try to import any Mathbin module, I get an error like this:
object file './lean_packages/mathlib/./build/lib/Mathlib.olean' of module Mathlib does not exist
What am I doing wrong?
Alexander Bentkamp (Jan 28 2022 at 13:46):
Ok, I've figured it out although I do not understand why: I need to write an import of a Mathlib module into any file first, e.g.,
import Mathlib.Algebra.Group.Basic
Once I have done that, the problem is resolved and I can then import any Mathbin module. I can even delete the Mathlib import later.
Gabriel Ebner (Jan 28 2022 at 14:57):
./lean_packages/mathlib/././Mathlib/Util/Export.lean:197:51: error: unknown identifier 'default'
This looks like you have the wrong Lean version. What does your lean-toolchain file say?
Alexander Bentkamp (Jan 28 2022 at 16:10):
leanprover/lean4:nightly-2022-01-27
Gabriel Ebner (Jan 28 2022 at 16:14):
LEAN_PATH=./lean_packages/mathlib/./build/lib /Users/alex/.elan/toolchains/leanprover--lean4---nightly-2021-10-29/bin/lean -R ./lean_packages/mathlib/./. -o ./lean_packages/mathlib/./build/lib/Mathlib/Util/TermUnsafe.olean ./lean_packages/mathlib/././Mathlib/Util/TermUnsafe.lean
This says October 29 ^^
Alexander Bentkamp (Jan 28 2022 at 16:16):
Hm, ok, I am rerunning it now to see whether I messed up earlier.
Alexander Bentkamp (Jan 28 2022 at 16:17):
Anyway, I got it working for me now. I am just trying again to see why it went wrong.
Alexander Bentkamp (Jan 28 2022 at 16:19):
Ok, I can't reproduce the issue. I probably got the Lean version wrong earlier although that doesn't fully explain what happened. Sorry for the trouble!
Last updated: Dec 20 2023 at 11:08 UTC