search

UniFormal / MMT

The MMT Language and System
https://uniformal.github.io/
Other
68 stars 23 forks source link

Metadata given in surface syntax is not persisted in OMDoc #528

Closed ComFreek closed 3 years ago

ComFreek commented 4 years ago

For example in FrameIT/FrameWorld we have

theory ScrollMeta : ?FactCollection =
  include ☞http://mathhub.info/MitM/Foundation?Strings ❙

  name  ❙
  description ❙
  problemTheory ❙
  solutionTheory ❙
❚
theory OppositeLen_Solution : ?ScrollMeta =
    meta http://mathhub.info/FrameIT/frameworld?ScrollMeta?name "OppositeLen" ❙
    meta http://mathhub.info/FrameIT/frameworld?ScrollMeta?problemTheory ?OppositeLen_Problem ❙
    meta http://mathhub.info/FrameIT/frameworld?ScrollMeta?solutionTheory ?OppositeLen_Solution ❙
    meta http://mathhub.info/FrameIT/frameworld?ScrollMeta?description "Given a triangle ABC right angled at C, the distance AB can be computed from the angle at B and the distance BC" ❙
❚

Steps to reproduce

  1. Build the above file (e.g. in MMT shell, but from Scala code it also works), now the meta keys are in-memory
  2. Terminate that shell/Scala program
  3. Now read that archive again without building and the meta keys specified in surface syntax above are gone.

By contrast, the meta keys for source information are still available.

ComFreek commented 3 years ago

Fixed in https://github.com/UniFormal/MMT/commit/ea8782d6a4827a6641321990f818d22917dc04d6.