display certifiable proofs with xsl transformation

[jwaldmann]

this should be used for display: http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/CPF/raw-file/tip/cpfHTML.xsl

how do we recognize the outputs where this should be applied? officially, we'd have to look at the category (whether it's certified) but we can just look at the second line of output (for <xml> tag).

note: need to strip off timestamps, and first line (YES), and last line (EOF), similar to https://github.com/jwaldmann/ceta-postproc/blob/master/Main.hs#L86

[stefanvonderkrone]

Any example job-pair? Or which solver/config should I use?

[jwaldmann]

anything from here: http://nfa.imn.htwk-leipzig.de/termcomp-devel/show_job_results/4067

beware: older matchbox output is in xml format, but does not contain the xsl reference (but it's fixed in tool/config 1790/2846)

[stefanvonderkrone]

As for now, I would rely on the new version...

[jwaldmann]

yes that's enough. it was just a warning that the transformation might fail for data from previous test runs.

[stefanvonderkrone]

see c7a1fe7dff050c02ca964b94e277eb406216dca5 html- and xml-proofs can now be displayed

[jwaldmann]

does it work? I don't think my browser finds the xsl file.

[stefanvonderkrone]

Please try again, I hope, that this is now fixed

[jwaldmann]

OK, works: http://nfa.imn.htwk-leipzig.de/termcomp-devel/display_proof/22951423

There are still problems with http://nfa.imn.htwk-leipzig.de/termcomp-devel/display_proof/22951421 but that's because TTT2 has a very long description. This is not an issue for us (requires change in TTT2 or in cpfHTML), thus closing.

[stefanvonderkrone]

Yes, I think this is a problem with TTT2 or the xsl

[jwaldmann]

meanwhile I think it's not "additional stuff" - it's perfectly valid contents according to the schema:

                   <xs:element maxOccurs="unbounded" name="tool">
                      <xs:complexType>
                        <xs:sequence>
                          <xs:element name="name" type="xs:string"/>
                          <xs:element name="version" type="xs:string"/>
                          <xs:element minOccurs="0" name="strategy" type="xs:string"/>
                          <xs:element minOccurs="0" ref="url"/>
                        </xs:sequence>
                      </xs:complexType>
                    </xs:element>
                    <xs:element maxOccurs="unbounded" minOccurs="0" name="toolUser">
                      <xs:complexType>
                        <xs:sequence>
                          <xs:element name="firstName" type="xs:string"/>
                          <xs:element name="lastName" type="xs:string"/>
                          <xs:element minOccurs="0" ref="url"/>
                        </xs:sequence>
                      </xs:complexType>
                    </xs:element>

it just needs better display (change in cpfHTML)