egg, missing files

Stream: general

[Jared green]

in a file importing only lean-egg, i get this error(having installed the latest version of rust on windows)
c:\Users\jared\.elan\toolchains\leanprover--lean4---v4.15.0\bin\lake.exe setup-file C:/Users/jared/lean projects/polySat/PolySat/egg_test.lean Init Egg failed:

stderr:
✖ [2/181] Running egg/egg_for_lean.static
trace: .\.\.lake/packages\egg\Rust\Egg> cargo rustc --release -- -C relocation-model=pic
info: stderr:
Compiling egg-for-lean v0.1.0 (C:\Users\jared\lean projects\polySat\.lake\packages\egg\Rust\Egg)
error[E0433]: failed to resolve: could not find unix in os
--> build.rs:3:14
|
3 | use std::os::unix::ffi::OsStrExt;
| ^^^^ could not find unix in os
|
note: found an item that was configured out
--> /rustc/9fc6b43126469e3858e2fe86cafb4f0fd5068869\library\std\src\os\mod.rs:36:9
note: the item is gated here
--> /rustc/9fc6b43126469e3858e2fe86cafb4f0fd5068869\library\std\src\os\mod.rs:28:1
note: found an item that was configured out
--> /rustc/9fc6b43126469e3858e2fe86cafb4f0fd5068869\library\std\src\os\mod.rs:85:9
note: the item is gated here
--> /rustc/9fc6b43126469e3858e2fe86cafb4f0fd5068869\library\std\src\os\mod.rs:84:1

error[E0599]: no function or associated item named from_bytes found for struct OsStr in the current scope
--> build.rs:11:20
|
11 | let s = OsStr::from_bytes(&bytes).to_str().unwrap();
| ^^^^^^^^^^ function or associated item not found in OsStr

Some errors have detailed explanations: E0433, E0599.
For more information about an error, try rustc --explain E0433.
error: could not compile egg-for-lean (build script) due to 2 previous errors
error: external command 'cargo' exited with code 101
✖ [6/181] Running egg/slotted_for_lean.static
trace: .\.\.lake/packages\egg\Rust\Slotted> cargo rustc --release -- -C relocation-model=pic
info: stderr:
Finished release profile [optimized] target(s) in 0.01s
error: no such file or directory (error code: 2)
file: .\.\.lake/packages\egg\Rust\Slotted\target\release\slotted_for_lean.a
✖ [10/181] Building egg/importTarget
trace: .> cc -c -o .\.\.lake/packages\egg\.lake\build\c\ffi.o .\.\.lake/packages\egg\C\ffi.c -I c:\Users\jared\.elan\toolchains\leanprover--lean4---v4.15.0\include -fPIC
error: failed to execute 'cc': no such file or directory (error code: 2)
Some required builds logged failures:

• egg/egg_for_lean.static
• egg/slotted_for_lean.static
• egg/importTarget
  error: build failed

[Marcus Rossel]

@memoryleak47 that seems to be a problem with building the reverse-ffi part:

3 | use std::os::unix::ffi::OsStrExt;
| ^^^^ could not find unix in os

Does this part have to be OS-dependent?

let s = OsStr::from_bytes(&bytes).to_str().unwrap();

And if so, do you happen to know if we can conditionally import std::os::windows build in the same way otherwise?

[Jared green]

could you also make it work on the mac, as on my mac i get the same error message almost verbatim

[Marcus Rossel]

huh, ok that's unexpected. I'm also on mac

[Jared green]

i actually get a different error, because i couldnt update rust on mine.

[Jared green]

so i got a new computer and tried it there

[Jared green]

this is the error message from my mac:/Users/programr/.elan/toolchains/leanprover--lean4---v4.15.0/bin/lake setup-file /Users/programr/polySat/PolySat/egg_test.lean Init Egg failed:

stderr:
✖ [2/181] Running egg/egg_for_lean.static
trace: ././.lake/packages/egg/Rust/Egg> cargo rustc --release -- -C relocation-model=pic
info: stderr:
warning: unused manifest key: package.edition
Updating registry https://github.com/rust-lang/crates.io-index
error: An unknown error occurred

Caused by:
Features and dependencies cannot have the same name: jobserver

To learn more, run the command again with --verbose.
error: external command 'cargo' exited with code 101
✖ [6/181] Running egg/slotted_for_lean.static
trace: ././.lake/packages/egg/Rust/Slotted> cargo rustc --release -- -C relocation-model=pic
info: stdout:
Build failed, waiting for other jobs to finish...
info: stderr:
warning: unused manifest key: package.edition
Updating registry https://github.com/rust-lang/crates.io-index
Downloading libc v0.2.169
Downloading slotted-egraphs v0.0.26
Downloading fnv v1.0.7
Compiling fnv v1.0.7
Compiling libc v0.2.169
error: there is no argument named vers
--> /Users/programr/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.169/build.rs:56:9
|
56 | println!("cargo:warning=setting FreeBSD version to {vers}");
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
= note: this error originates in a macro outside of the current crate

error: aborting due to previous error

error: Could not compile libc.
error: build failed
error: external command 'cargo' exited with code 101
✔ [11/181] Built egg/importTarget
✔ [12/181] Built egg/ffi.static
✔ [14/181] Built ffi.static:shared
✔ [163/181] Built Calcify.Basic
✔ [164/181] Built Calcify
✔ [178/181] Built Calcify:c.o
✔ [179/181] Built Calcify.Basic:c.o
✔ [180/181] Built Calcify.Basic:dynlib
✔ [181/181] Built Calcify:dynlib
Some required builds logged failures:

• egg/egg_for_lean.static
• egg/slotted_for_lean.static
  error: build failed

[Violeta Hernández]

Marcus Rossel said:

memoryleak47 that seems to be a problem with building the reverse-ffi part:

3 | use std::os::unix::ffi::OsStrExt;
| ^^^^ could not find unix in os

Does this part have to be OS-dependent?

let s = OsStr::from_bytes(&bytes).to_str().unwrap();

And if so, do you happen to know if we can conditionally import std::os::windows build in the same way otherwise?

I don't see why this couldn't be replaced by String::from_utf8(&bytes).unwrap().

[Violeta Hernández]

(idk anything about egg, but I know some Rust)

[Rudi Schneider]

I don't see why this couldn't be replaced by String::from_utf8(&bytes).unwrap().

yes, sorry! I can change that

[Rudi Schneider]

should be a rather uncontroversial fix, I assume https://github.com/marcusrossel/lean-egg/pull/59 @Marcus Rossel

[Marcus Rossel]

Thanks :)

[Jared green]

i still get errors:
c:\Users\jared\.elan\toolchains\leanprover--lean4---v4.15.0\bin\lake.exe setup-file C:/Users/jared/lean projects/polySat/PolySat/egg_test.lean Init Egg failed:

stderr:
✖ [2/181] Running egg/egg_for_lean.static
trace: .\.\.lake/packages\egg\Rust\Egg> cargo rustc --release -- -C relocation-model=pic
info: stderr:
Compiling egg-for-lean v0.1.0 (C:\Users\jared\lean projects\polySat\.lake\packages\egg\Rust\Egg)
warning: egg-for-lean@0.1.0: cl : Command line warning D9002 : ignoring unknown option '-fstack-clash-protection'
warning: egg-for-lean@0.1.0: cl : Command line warning D9002 : ignoring unknown option '-fwrapv'
error: failed to run custom build command for egg-for-lean v0.1.0 (C:\Users\jared\lean projects\polySat\.lake\packages\egg\Rust\Egg)

(there is more but its way too long for a single comment)

[Jared green]

i attach the rest.
egg_error.txt

[Jared green]

after installing gcc, i now get this:

`c:\Users\jared\.elan\toolchains\leanprover--lean4---v4.15.0\bin\lake.exe setup-file C:/Users/jared/lean projects/polySat/PolySat/egg_test.lean Init Egg` failed:

stderr:
✖ [2/181] Running egg/egg_for_lean.static
trace: .\.\.lake/packages\egg\Rust\Egg> cargo rustc --release -- -C relocation-model=pic
info: stderr:
Compiling egg-for-lean v0.1.0 (C:\Users\jared\lean projects\polySat\.lake\packages\egg\Rust\Egg)
warning: egg-for-lean@0.1.0: cl : Command line warning D9002 : ignoring unknown option '-fstack-clash-protection'
warning: egg-for-lean@0.1.0: cl : Command line warning D9002 : ignoring unknown option '-fwrapv'
error: failed to run custom build command for `egg-for-lean v0.1.0 (C:\Users\jared\lean projects\polySat\.lake\packages\egg\Rust\Egg)`

Caused by:
  process didn't exit successfully: `c:\Users\jared\lean projects\polySat\.lake\packages\egg\Rust\Egg\target\release\build\egg-for-lean-78a07c5dafb7be3c\build-script-build` (exit code: 1)

...

  --- stderr


  error occurred in cc-rs: Command "C:\\Program Files\\Microsoft Visual Studio\\2022\\Community\\VC\\Tools\\MSVC\\14.42.34433\\bin\\HostX64\\x64\\cl.exe" "-nologo" "-MD" "-O2" "-Brepro" "-W4" "-I" "c:\\Users\\jared\\.elan\\toolchains\\leanprover--lean4---v4.15.0\\include" "-fstack-clash-protection" "-fwrapv" "-Foc:\\Users\\jared\\lean projects\\polySat\\.lake\\packages\\egg\\Rust\\Egg\\target\\release\\build\\egg-for-lean-e85d41a1d5581826\\out\\a7d9c1e0c091b9d8-rev_ffi.o" "-c" "../../C/rev_ffi.c" with args cl.exe did not execute successfully (status code exit code: 2).
error: external command 'cargo' exited with code 101
✖ [6/181] Running egg/slotted_for_lean.static
trace: .\.\.lake/packages\egg\Rust\Slotted> cargo rustc --release -- -C relocation-model=pic
info: stderr:
Finished `release` profile [optimized] target(s) in 0.01s
error: no such file or directory (error code: 2)
  file: .\.\.lake/packages\egg\Rust\Slotted\target\release\slotted_for_lean.a
✔ [17/181] Built egg/importTarget
✔ [18/181] Built egg/ffi.static
✖ [20/181] Building ffi.static:shared
trace: .> c:\Users\jared\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe -shared -o .\.\.lake/packages\egg\.lake\build\lib\ffi.dll -Wl,--whole-archive .\.\.lake/packages\egg\.lake\build\lib\ffi.a -Wl,--no-whole-archive
info: stderr:
ld.lld: error: undefined symbol: egg_free_egraph
>>> referenced by ffi.a(ffi.o):(egg_egraph_finalize)

ld.lld: error: undefined symbol: slotted_free_egraph
>>> referenced by ffi.a(ffi.o):(slotted_egraph_finalize)

ld.lld: error: undefined symbol: slotted_explain_congr
>>> referenced by ffi.a(ffi.o):(run_eqsat_request_core)

ld.lld: error: undefined symbol: egg_explain_congr
>>> referenced by ffi.a(ffi.o):(run_eqsat_request_core)

ld.lld: error: undefined symbol: slotted_query_equiv
>>> referenced by ffi.a(ffi.o):(explain_equiv)

ld.lld: error: undefined symbol: egg_query_equiv
>>> referenced by ffi.a(ffi.o):(explain_equiv)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command 'c:\Users\jared\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe' exited with code 1
Some required builds logged failures:
- egg/egg_for_lean.static
- egg/slotted_for_lean.static
- ffi.static:shared
error: build failed

[Ruben Van de Velde]

Please use backticks to show console output

[Jared green]

what is a backtick?

[Andrés Goens]

@Jared green a backtick is this character: ` you can use three of them to start a block that is console output, and then there more (in a single line) when it ends, e.g.:

this is some console output

[Andrés Goens]

(if you click on the dots on the top right of the message and select "view original message" you can see how that works)

[Andrés Goens]

error: no such file or directory (error code: 2)
  file: .\.\.lake/packages\egg\Rust\Slotted\target\release\slotted_for_lean.a

ahh, that looks like the culprit! It looks like we're currently assuming posix format (with the .a), and on windows that would become something else (I don't know what static libraries are called in windows), I guess no one had tried this on windows before :/

[Jared green]

what can i do about it?

[Marcus Rossel]

Andrés Goens said:

error: no such file or directory (error code: 2)
  file: .\.\.lake/packages\egg\Rust\Slotted\target\release\slotted_for_lean.a

ahh, that looks like the culprit! It looks like we're currently assuming posix format (with the .a), and on windows that would become something else (I don't know what static libraries are called in windows), I guess no one had tried this on windows before :/

I don't think that's the underlying problem. We're using nameToStaticLib in the lakefile, which should account for Windows.

[Sebastian Ullrich]

It may also be .lib on Windows

[Marcus Rossel]

Jared green said:

i attach the rest.
egg_error.txt

This also contains a bunch of errors when building lean.h...?

  c:\Users\jared\.elan\toolchains\leanprover--lean4---v4.15.0\include\lean/lean.h(204): error C2061: syntax error: identifier '_Atomic'
  c:\Users\jared\.elan\toolchains\leanprover--lean4---v4.15.0\include\lean/lean.h(205): error C2061: syntax error: identifier 'm_closure'
  c:\Users\jared\.elan\toolchains\leanprover--lean4---v4.15.0\include\lean/lean.h(205): error C2059: syntax error: ';'
  c:\Users\jared\.elan\toolchains\leanprover--lean4---v4.15.0\include\lean/lean.h(206): error C2059: syntax error: '}'
  c:\Users\jared\.elan\toolchains\leanprover--lean4---v4.15.0\include\lean/lean.h(276): error C2061: syntax error: identifier '_Atomic'
  c:\Users\jared\.elan\toolchains\leanprover--lean4---v4.15.0\include\lean/lean.h(278): error C2059: syntax error: '}'
  c:\Users\jared\.elan\toolchains\leanprover--lean4---v4.15.0\include\lean/lean.h(307): warning C4431: missing type specifier - int assumed. Note: C no longer supports default-int
  c:\Users\jared\.elan\toolchains\leanprover--lean4---v4.15.0\include\lean/lean.h(307): error C2054: expected '(' to follow '_Noreturn'
  c:\Users\jared\.elan\toolchains\leanprover--lean4---v4.15.0\include\lean/lean.h(307): error C2085: 'lean_internal_panic': not in formal parameter list
  c:\Users\jared\.elan\toolchains\leanprover--lean4---v4.15.0\include\lean/lean.h(308): error C2061: syntax error: identifier '_Noreturn'
...

[Marcus Rossel]

Sebastian Ullrich said:

It may also be .lib on Windows

Would that have to be changed in Lake's nameToStaticLib then?