leanprover-community / format_lean Goto Github PK

View Code? Open in Web Editor NEW

59.0 59.0 8.0 116 KB

A Lean file formatter

Home Page: https://leanprover-community.github.io/format_lean/

License: Apache License 2.0

CSS 7.41% JavaScript 3.16% Python 66.48% Shell 0.24% HTML 1.89% SCSS 20.83%

format_lean's People

Contributors

Stargazers

Watchers

Forkers

kodyvajjha mpedramfar jesse-michael-han utensil winston-h-zhang hotdogontology seanpm2001 dallin-mclaughlin

format_lean's Issues

trouble with Ubuntu

The default python on Ubuntu is 3.6. I can install 3.7 (or rather the worryingly-named python3.7-minimal) using apt but my ipython seems to use 3.6. Of course I can use python 3.7 by just typing python3.7. Here's a session:

format_lean/src$ python3.7
Python 3.7.1 (default, Oct 22 2018, 11:21:55) 
[GCC 8.2.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> from format_lean.lecture import render_lean_file
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/home/buzzard/Encfs/Computer_languages/python/format_lean/src/format_lean/lecture.py", line 7, in <module>
    import regex
ModuleNotFoundError: No module named 'regex'
Error in sys.excepthook:
Traceback (most recent call last):
  File "/usr/lib/python3/dist-packages/apport_python_hook.py", line 63, in apport_excepthook
    from apport.fileutils import likely_packaged, get_recent_crashes
  File "/usr/lib/python3/dist-packages/apport/__init__.py", line 5, in <module>
    from apport.report import Report
  File "/usr/lib/python3/dist-packages/apport/report.py", line 30, in <module>
    import apport.fileutils
  File "/usr/lib/python3/dist-packages/apport/fileutils.py", line 23, in <module>
    from apport.packaging_impl import impl as packaging
  File "/usr/lib/python3/dist-packages/apport/packaging_impl.py", line 24, in <module>
    import apt
  File "/usr/lib/python3/dist-packages/apt/__init__.py", line 23, in <module>
    import apt_pkg
ModuleNotFoundError: No module named 'apt_pkg'

Original exception was:
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/home/buzzard/Encfs/Computer_languages/python/format_lean/src/format_lean/lecture.py", line 7, in <module>
    import regex
ModuleNotFoundError: No module named 'regex'
>>>

I have never used pip3 before, but I have it installed.

I suspect that the problem is that python3.7 is not being used globally. However I can't get the instructions on how to move to a 3.7 environment to work either. pip3 install --user virtualenvwrapper works fine, export VIRTUALENVWRAPPER_VIRTUALENV=/usr/local/bin/virtualenv looks fishy to me because the only virtualenv I can find on my system is in /usr/bin/, but replacing /usr/local/bin with /usr/bin and continuing gives me

$ source $HOME/.local/bin/virtualenvwrapper.sh
/usr/bin/python: No module named virtualenvwrapper
virtualenvwrapper.sh: There was a problem running the initialization hooks.

If Python could not import the module virtualenvwrapper.hook_loader,
check that virtualenvwrapper has been installed for
VIRTUALENVWRAPPER_PYTHON=/usr/bin/python and that PATH is
set properly.

and /usr/bin/python is still Python 2.7 on Ubuntu.

Python 3.6?

I've looked at deploying this on cocalc, but the python 3.7 dependency isn't given without much extra work. I saw there are just two mall usages of that @dataclass. Despite that it is a cool new feature, maybe we could go back to the traditional style and make installing it much easier?

Besides that, is there are test to run? To me this looks like something where a small test with integration to travis-ci could be worthwhile to add.

fire up ipython in src

In usage in the README, I think you need to fire up ipython from within src to get the import to work.

Having trouble with example formatter

On Ubuntu 18.04, which still has python3.6 as default. I've installed packages python3.7 and python3-pip and ipython3 (although I don't know for sure whether python3-pip will use python 3.6 by default etc etc :-( ).

format_lean$ pip3 install . seemed to go fine, it returned

Successfully installed Lean-formatter-0.0.1 MarkupSafe-1.1.0 jinja2-2.10 regex-2019.2.7

but in ipython3 I get

In [1]: from format_lean.lecture import render_lean_file
---------------------------------------------------------------------------
ModuleNotFoundError                       Traceback (most recent call last)
<ipython-input-1-662f8a35540b> in <module>()
----> 1 from format_lean.lecture import render_lean_file

ModuleNotFoundError: No module named 'format_lean'

Sandwich Theorem Typo

Shouldn't the |bn-l| be |cn-l| in the last second line of Sandwich Theorem?

subdirectories of src

I have a Lean project, with files sandwich.lean and src/M40001/sandwich.lean and these are identical files. I'm in the root directory of the project (the directory which contains sandwich.lean).

format_lean. If I type

format_lean --inpath sandwich.lean --outdir html --lib-path _target/deps/mathlib/src/

then everything works fine. The contents of the html directory are

colorful.css   lecture.css      teach_lean.css      with_tufte.css.map
jquery.min.js  lecture.css.map  teach_lean.css.map
lean.js        sandwich.html    with_tufte.css

But if I type

format_lean --inpath src/M40001/sandwich.lean --outdir html --lib-path _target/deps/mathlib/src/

I get an error

FileNotFoundError: [Errno 2] No such file or directory: 'html/src/M40001/sandwich.html'

[note this is about html files] and if I try

format_lean --inpath M40001/sandwich.lean --outdir html --lib-path _target/deps/mathlib/src/

I get No such file or directory: 'M40001/sandwich.lean' [note this is about lean files] (and indeed there is no such file or directory as I am in the root directory).

Now I move the root sandwich.lean to src and I add format.toml in root containing the line only = ['sandwich.lean']. I type format_project and things work fine, although I will remark that my html directory looks like this now:

colorful.css   lean.js      lecture.css.map
jquery.min.js  lecture.css  sandwich.html

(far fewer files). It works fine.

But I still have this identical copy of sandwich.lean in src/M40001. If I edit format.toml so it says only = ['M40001/sandwich.lean'] and run format_project, I get an html file but nothing is clickable (i.e. I can't "open" the web page to see the tactics).

key error when rendering file

In [5]: render_lean_file('patrick.lean', toolchain='3.4.2', lib_path='/home/buzz
   ...: ard/Lean/lean-projects/mathlib-community-master/src')                   
---------------------------------------------------------------------------
KeyError                                  Traceback (most recent call last)
~/Encfs/Computer_languages/python/format_lean/src/format_lean/server.py in info(self, filename, line, col)
     31         try:
---> 32             return ret['record']['state']
     33         except KeyError:

KeyError: 'record'

During handling of the above exception, another exception occurred:

LeanError                                 Traceback (most recent call last)
<ipython-input-5-11d8be898351> in <module>
----> 1 render_lean_file('patrick.lean', toolchain='3.4.2', lib_path='/home/buzzard/Lean/lean-projects/mathlib-community-master/src')

~/Encfs/Computer_languages/python/format_lean/src/format_lean/lecture.py in render_lean_file(inpath, outpath, toolchain, lib_path, templates)
    310              DefinitionEnd, LemmaBegin, LemmaEnd, ProofBegin, ProofEnd,
    311              ProofComment])
--> 312     lecture_reader.read_file(inpath)
    313     renderer = Renderer.from_file(templates)
    314     renderer.render(lecture_reader.output, outpath)

~/Encfs/Computer_languages/python/format_lean/src/format_lean/line_reader.py in read_file(self, path)
     43                         self.blank_line_handler(self, line)
     44                     else:
---> 45                         self.normal_line_handler(self, line)
     46                 self.cur_line_nb += 1
     47 

~/Encfs/Computer_languages/python/format_lean/src/format_lean/lecture.py in normal_line(file_reader, line)
    283             file_reader.status = 'proof'
    284             tsl = file_reader.server.info(file_reader.filename,
--> 285                     file_reader.cur_line_nb, 1)
    286             tsr = file_reader.server.info(file_reader.filename,
    287                     file_reader.cur_line_nb, len(line))

~/Encfs/Computer_languages/python/format_lean/src/format_lean/server.py in info(self, filename, line, col)
     32             return ret['record']['state']
     33         except KeyError:
---> 34             raise LeanError(str(ret))

LeanError: {'msgs': [{'caption': '', 'file_name': '/home/buzzard/Encfs/Computer_languages/Lean/lean-projects/mathlib-community-master/src/data/set/basic.lean', 'pos_col': 53, 'pos_line': 621, 'severity': 'error', 'text': '(deterministic) timeout'}, {'caption': '', 'file_name': '/home/buzzard/Encfs/Computer_languages/Lean/lean-projects/mathlib-community-master/src/data/set/basic.lean', 'pos_col': 3, 'pos_line': 622, 'severity': 'error', 'text': '(deterministic) timeout'}], 'response': 'all_messages'}

This is when trying to compile patrick.lean, the file at https://www.math.u-psud.fr/~pmassot/lean/source.html. There is a pause of around 15-20 seconds before I get the error, making me think that something is happening.

lean to other formal language

Would be possible to use ideas from here to produce TPTP (http://tptp.org) from Lean files? Of course, the transformation would need to deal with the proper mapping from dependent types to FOL, THF etc.

leanprover-community / format_lean Goto Github PK

format_lean's People

Contributors

Stargazers

Watchers

Forkers

format_lean's Issues

trouble with Ubuntu

Python 3.6?

fire up ipython in src

Having trouble with example formatter

Sandwich Theorem Typo

subdirectories of src

key error when rendering file

lean to other formal language

Recommend Projects

React

Vue.js

Typescript

TensorFlow

Django

Laravel

D3

Recommend Topics

javascript

web

server

Machine learning

Visualization

Game

Recommend Org

Facebook

Microsoft

Google

Alibaba

D3

Tencent