Generate abstr/ directory

digama0 / mizar-rs

Alternative Mizar proof checker (http://mizar.org/) written in Rust

GNU General Public License v3.0

47 stars 4 forks source link

Generate abstr/ directory #5

Open digama0 opened 1 year ago

digama0 commented 1 year ago

MML comes with a abstr/ directory containing:

abstr/foo.abs for each article foo
abstr/reftags
abstr/symbtags

It is a mystery how these files are generated, since the build script is not available anywhere that I can find. I believe the foo.abs file is obtained by using absedt, but I cannot find any tool that seems likely to be able to generate nor consume the reftags and symbtags files, although it's not too hard to take some guesses about the format.

CoghettoR commented 1 year ago

for emacs completion (in mizar.el)

line 1839 and 1841: https://github.com/JUrban/mizarmode/blob/master/mizar.el

Generation: https://github.com/JUrban/mizarmode/blob/master/stag.pl