search

david-a-wheeler / mmverify.py

Metamath verifier in Python
MIT License
35 stars 10 forks source link

This software no longer works with Python 3.x #17

Closed enjoysmath closed 1 year ago

enjoysmath commented 2 years ago

Hi,

I converted all list[Type] to List[Type] where List is imported from typing, etc. But I'm getting the following error with Python 3.x:

 File "C:\Users\fruit\OneDrive\Desktop\mmverify.py\mmverify.py", line 683, in <module>
  mm.read(Toks(db_file))
 File "C:\Users\fruit\OneDrive\Desktop\mmverify.py\mmverify.py", line 96, in __init__
  self.imported_files = set({pathlib.Path(str(file.name)).resolve()})
File "C:\Python38\Lib\pathlib.py", line 1159, in resolve
  s = self._flavour.resolve(self, strict=strict)
File "C:\Python38\Lib\pathlib.py", line 202, in resolve
  s = self._ext_to_normal(_getfinalpathname(s))

builtins.OSError: [WinError 123] The filename, directory name, or volume label syntax is incorrect: '<stdin>'

image

Please help me get this to run using Python 3.x. I just want to run the verifier as a prototype for a version in the language D.

I can probably understand most of the code without the working prototype though.

david-a-wheeler commented 2 years ago

Can you create a pull request with the work so far?

enjoysmath commented 2 years ago

@david-a-wheeler I decided to instead use the mmverify.py linked to on metamath's homepage. That one works with Python3 and is also less lines :) I really just need a prototype to look at. Python is not ideal proof search, mass verification, etc. So I was going to write this in D and use pegged to specify the EBNF of Metamath.