message in mathlib3port file

Stream: mathlib4

[Chris Birkbeck]

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]

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]

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]

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]

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

[Chris Birkbeck]

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]

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]

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]

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]

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]

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]

Did you run make source first?

[Scott Morrison]

The makefile should probably have an explicit dependency.

[Jon Eugster]

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]

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]

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

[Jireh Loreaux]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

You want to use oneshot for this.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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