eds.activemath.org

Now, this is a great day! SLuMB, the OMDoc file storage for ActiveMath supports <imports from="x" type="global"/>. This was a standard feature of OMDoc specification but was never supported. I finally understood that this is the clean-way to support the management of big files and I even successfully split a LeAM_calculus monster-file in two without breaking references.

Basically, here’s what one can do, taken from jEditOQMath’s chapter 6:

Suppose we are within <theory id="A"> and use the imports statement <imports from="mbase://openmath-cds/set1" type="global"/>. Then within a theory <theory id="B"> having an import <import from="A"> all the names of the theory A are visible, including the globally imported ones, so including set which is a reference to the symbol of id mbase://openmath-cds/set1/set.

Such an approach is particularly nifty to declare names theories that gather all the classical names used within, say, many files of a collection.

Applying to your collections

It is important to note that until very recently all imports were actually marked global in the DTD… Hence SLuMB was made tolerant to imports’ cycles even though they are very bad practice in principle.

In order to split a big file, split it in two kinds of files:

• a names file which basically imports all the others
• other files which contain the items

the names file should contain the theory with the original name and import the other files, with type global. All the references that were to the names file will now be absolutized to the revised one, as one wishes.

Feedback welcome.

This feature is part of ActiveMath-SVN since Friday.