Zulip Chat Archive

Stream: mathlib4

Topic: message in mathlib3port file


Chris Birkbeck (Nov 21 2022 at 14:59):

I was thinking of trying to port a file to see what its like. I made some import graphs and control.monad.basic seems to have all of its dependencies done. The thing is on the mathlib3port file it has the following message, which I don't understand:

/- ./././Mathport/Syntax/Translate/Tactic/Mathlib/Core.lean:61:9: unsupported: weird string -/
/- failed to parenthesize: unknown constant 'Lean.Meta._root_.Lean.Parser.Command.registerSimpAttr'
[PrettyPrinter.parenthesize.input] (Lean.Meta._root_.Lean.Parser.Command.registerSimpAttr
     [(Command.docComment
       "/--"
       "./././Mathport/Syntax/Translate/Tactic/Mathlib/Core.lean:61:9: unsupported: weird string -/")]
     "register_simp_attr"
     `monad_norm)-/-- failed to format: unknown constant 'Lean.Meta._root_.Lean.Parser.Command.registerSimpAttr'
/-- ./././Mathport/Syntax/Translate/Tactic/Mathlib/Core.lean:61:9: unsupported: weird string -/

What should I do about this? should I just look for something else to work on?

Ruben Van de Velde (Nov 21 2022 at 15:04):

Looks like it's choking on the mk_simp_attribute - I'd be inclined to translate just the lemma/defs, but maybe someone who knows more about this could chime in

Mario Carneiro (Nov 21 2022 at 18:00):

Errors of the form "failed to parenthesize" / "failed to format" are always bugs in mathport, usually because some syntax changed in mathlib and hasn't yet been updated in mathport

Mario Carneiro (Nov 21 2022 at 18:02):

the "unsupported: weird string" error means that there was a string literal expected but the code uses some more unusual way of constructing the string in the original code. What's the input lean 3 expression?

Jireh Loreaux (Nov 21 2022 at 18:07):

How do you want us to report these to you? And is there any troubleshooting we should do to determine the cause?

Chris Birkbeck (Nov 21 2022 at 18:14):

Mario Carneiro said:

the "unsupported: weird string" error means that there was a string literal expected but the code uses some more unusual way of constructing the string in the original code. What's the input lean 3 expression?

I'm not 100% sure, but the thing closest to this message is mk_simp_attribute monad_norm none with functor_norm

Mario Carneiro (Nov 21 2022 at 18:20):

Jireh Loreaux said:

How do you want us to report these to you? And is there any troubleshooting we should do to determine the cause?

A small file that fails in mathport oneshot would be great

Jireh Loreaux (Nov 21 2022 at 18:24):

Okay, the steps to use oneshot are the following, correct?

  1. clone the mathport repo
  2. make predata
  3. lake build
  4. write the file you want to oneshot to Oneshot/lean3-in/main.lean
  5. (optional) write a Lean 4 file with #aligns to Oneshot/lean4-in/Oneshot.lean
  6. make oneshot

I saw something in the README about an assumption about versions matching. What is the easy way to check I have the versions correct?

Mario Carneiro (Nov 21 2022 at 18:47):

you should use the ./download-release.sh script to be able to skip the make predata which amounts to a full compile of mathlib

Ruben Van de Velde (Nov 21 2022 at 20:30):

Mario Carneiro said:

the "unsupported: weird string" error means that there was a string literal expected but the code uses some more unusual way of constructing the string in the original code. What's the input lean 3 expression?

FTR: https://github.com/leanprover-community/mathlib/blob/2a1e571fb49995ef245be2b17745972dc981efb8/src/control/monad/basic.lean#L38

Jon Eugster (Nov 24 2022 at 10:10):

me@mycomputer: ~/XXX/mathport$ make oneshot
cd Oneshot/lean3-in && elan override set `cat ../../sources/mathlib/leanpkg.toml | grep lean_version | cut -d '"' -f2`
cat: ../../sources/mathlib/leanpkg.toml: No such file or directory

When following these steps, I got the error above. I then copied the leanpkg.toml manually from a mathlib-clone to fix it. Did I do something wrong?

(These steps means: what @Jireh Loreaux described, but replacing 2 and 3 with ./download-release.sh nightly-2022-11-23)

Scott Morrison (Nov 24 2022 at 15:05):

Did you run make source first?

Scott Morrison (Nov 24 2022 at 15:07):

The makefile should probably have an explicit dependency.

Jon Eugster (Nov 25 2022 at 12:36):

Scott Morrison said:

Did you run make source first?

I didn't. Now make oneshot complains about several missing log files. Anyways, it doesn't matter, I don't think I need oneshot at the moment

Kevin Buzzard (Dec 03 2022 at 14:16):

I cloned mathport and optimistically tried make predata; after seemingly downloading mathlib I got the following error (I truncated the full output):

mkdir -p sources/lean/build/release
# Run cmake, to create `version.lean` from `version.lean.in`.
cd sources/lean/build/release && cmake ../../src
CMake Deprecation Warning at CMakeLists.txt:1 (cmake_minimum_required):
  Compatibility with CMake < 2.8.12 will be removed from a future version of
  CMake.

  Update the VERSION argument <min> value or use a ...<max> suffix to tell
  CMake that the project does not need compatibility with older versions.


-- The CXX compiler identification is GNU 11.3.0
-- The C compiler identification is GNU 11.3.0
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /usr/bin/c++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working C compiler: /usr/bin/cc - skipped
-- Detecting C compile features
-- Detecting C compile features - done
-- No build type selected, default to Release
-- Lean library will be installed at /usr/local/lib/lean
CMake Error at cmake/Modules/FindGMP.cmake:7 (find_library):
  Could not find GMP_LIBRARIES using the following names: gmp, libgmp, mpir
Call Stack (most recent call first):
  CMakeLists.txt:296 (find_package)


-- Configuring incomplete, errors occurred!
See also "/home/buzzard/lean-projects/mathport/sources/lean/build/release/CMakeFiles/CMakeOutput.log".
make: *** [Makefile:62: lean3-source] Error 1

Any ideas?

Kevin Buzzard (Dec 03 2022 at 14:18):

Aah got it: sudo apt-get install libgmp3-dev gets me this multiprecision library which is apparently what was missing.

Jireh Loreaux (Dec 03 2022 at 14:35):

Note, you don't want to make predata, use the download_release script. See above.

Kevin Buzzard (Dec 03 2022 at 14:43):

What if I want to run the port on some random commit of mathlib which isn't even on the master branch?

Kevin Buzzard (Dec 03 2022 at 14:52):

To un-xy: I was simply idly wondering whether I could get a quick opinion from mathport about how to port the changes to combinatorics.quiver.basic here. Two lemmas were added to this file, which has been frozen. Obviously I could just port them by hand, but what's really going on is that I'm aware that as the tide rises we will find ourselves more and more often in the situation where some lemmas are going to need parallel mathlib3 and mathlib4 PRs and I was wondering how painful the process was to get a quick opinion.

Scott Morrison (Dec 03 2022 at 17:02):

You want to use oneshot for this.

Scott Morrison (Dec 03 2022 at 17:03):

(that is, for asking for a quick opinion on a handful of new lemmas)

Scott Morrison (Dec 03 2022 at 17:04):

Try Oneshot/README.md, but do make sure to use download_release as Jireh says, rather than running mathport on mathlib yourself.

Scott Morrison (Dec 03 2022 at 17:04):

If you have the right stuff downloaded, Oneshot is very fast.


Last updated: Dec 20 2023 at 11:08 UTC