search

MathHubInfo / Legacy-localmh

DEPRECATED - A cross-repository administration tool for the local authoring in MathHub.info
1 stars 0 forks source link

lmh tool for sTeX/MMT sync #310

Open kohlhase opened 7 years ago

kohlhase commented 7 years ago

We have started to build the MitM ontology by building an sTeX and an MMT theory graph that are name-synchronized. They are

  1. the SMGloM and
  2. the SMGloM formalization

files in 2. correspond to archives in 1. It would be good to have a lmh tool (e.g. lmh smdiff that applied to a file in 2. reports the lists of

and the same applied to 1. This is kind of a special-purpose theory/symbol-diff for the MitM. I will be working on this manually in the next weeks, so there will be a set of things to test this on soon.

kohlhase commented 7 years ago

Another facet of this functionality would be to generate raw theory skeletons to complete the respective other version, e.g. lmh smskel foo, where foo is a theory name and this would add a theory in MitM/smglom/source/bar.mmt in MitM or make files smglom/bar/source/foo.tex and smglom/bar/source/foo.en.tex in archive smglom/bar.