Can't find the output of exporting the Lean library in low level format.

[ITervaNkYu]

Prerequisites

• [ X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

I downloaded and unpacked the lean-3.4.1-linux.tar.gz. Then, per these instructions, I went to leanroot/lib/lean/library and typed

lean --export=export.out --recursive

However, I got the error below and I can't find the export.out file.

/home/user/Desktop/lean/lib/lean/library/init/data/ordering/default.lean:7:0: error: invalid import: init.data.ordering.basic invalid object declaration, environment already has an object named 'ordering' /home/user/Desktop/lean/lib/lean/library/init/data/ordering/default.lean:7:0: error: invalid import: init.data.ordering.basic invalid object declaration, environment already has an object named 'ordering' /home/user/Desktop/lean/lib/lean/library/init/data/ordering/default.lean:7:0: error: invalid import: init.data.ordering.basic invalid object declaration, environment already has an object named 'ordering' /home/user/Desktop/lean/lib/lean/library/init/data/ordering/default.lean:7:0: error: invalid import: init.data.ordering.basic invalid object declaration, environment already has an object named 'ordering' /home/user/Desktop/lean/lib/lean/library/init/data/char/classes.lean:7:0: error: invalid import: init.data.char.basic invalid object declaration, environment already has an object named 'is_valid_char' /home/user/Desktop/lean/lib/lean/library/init/data/char/classes.lean:7:0: error: invalid import: init.data.char.basic invalid object declaration, environment already has an object named 'is_valid_char' /home/user/Desktop/lean/lib/lean/library/init/data/char/classes.lean:7:0: error: invalid import: init.data.char.basic invalid object declaration, environment already has an object named 'is_valid_char' :1:1: error: invalid object declaration, environment already has an object named 'timeit'

Steps to Reproduce

Do as above.

Expected behavior: no error messages and export.out appears in the current directory

Actual behavior: Error messages and export.out cannot be found.

Reproduces how often: Only tried once.

Versions

Lean 3.4.1 Ubuntu 18.04.1 LTS

Additional Information