bug repro

6f3d60d4 · ComFreek · 934a92b0 · 6f3d60d4 · 6f3d60d4 · 6f3d60d4
Commit 6f3d60d4 authored 4 years ago by ComFreek
--- a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.omdoc.xz
--- a/errors/mmt-omdoc/IntegrationTests/thy-parameter-bug.mmt.err
+++ b/errors/mmt-omdoc/IntegrationTests/thy-parameter-bug.mmt.err
--- a/narration/IntegrationTests/thy-parameter-bug.omdoc
+++ b/narration/IntegrationTests/thy-parameter-bug.omdoc
+<?xml version="1.0" encoding="UTF-8"?>
+<omdoc base="http://mathhub.info/FrameIT/frameworld/IntegrationTests/thy-parameter-bug.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/thy-parameter-bug.mmt#0.0.0:277.10.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld/integrationtests"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/thy-parameter-bug.mmt#134.4.0:158.4.24"/></metadata></mref></omdoc>
\ No newline at end of file
--- a/relational/IntegrationTests/thy-parameter-bug.rel
+++ b/relational/IntegrationTests/thy-parameter-bug.rel
+document http://mathhub.info/FrameIT/frameworld/IntegrationTests/thy-parameter-bug.omdoc
+Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/thy-parameter-bug.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug
--- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.rel
+dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?A
+dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?B
+dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?dist
+theory http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug
+HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?A
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?A
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?A?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?A?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?B
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?B
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?B?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?B?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?dist
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?dist
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?dist?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?dist?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?dist?definition http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?dist?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?dist?definition http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?dist?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
--- a/source/IntegrationTests/SituationTheory.mmt
+++ b/source/IntegrationTests/SituationTheory.mmt
@@ -34,6 +34,4 @@ theory SampleSituationTheory =
        = ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ❘
                meta ?MetaAnnotations?label "distanceBC"
   ❙
-
-   test_simpl = d- A B ❙
 ❚
--- a/source/IntegrationTests/thy-parameter-bug.mmt
+++ b/source/IntegrationTests/thy-parameter-bug.mmt
+namespace http://mathhub.info/FrameIT/frameworld/integrationtests ❚
+
+fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta ❚
+
+theory TheoryParameterBug =
+    A = ⟨0.0, 0.0, 0.0⟩ ❙
+    B = ⟨3.0, 3.0, 0.0⟩ ❙
+
+    /T simplifying this constant fails: ❙
+    dist = d- A B ❙
+❚
\ No newline at end of file