Ticket #729 (closed task: fixed)

Opened 7 months ago

Last modified 6 months ago

Provide XML representation of development graph

Reported by: till Owned by: maeder
Priority: major Milestone: 0.95
Component: interfaces Version: 0.93
Keywords: Cc: autexier

Description


Change History

Changed 7 months ago by maeder

  • cc autexier added

I first version can be created using

hets -v2 -d DGraphXML Basic/Numbers.casl

Changed 7 months ago by maeder

  • status changed from new to assigned

Changed 6 months ago by maeder

  • status changed from assigned to closed
  • resolution set to fixed

xml output of the parsed library is created by the option "-o pp.xml", the development graph after "Proofs-Automatic" is obtained and output with "-o prf". The relpath attribute of nodes refers to the specs in the corresponding pp.xml file relative to a named spec or view (given as refname attribute).

maeder@leibniz:~/Hets> hets -v2 -o prf,pp.xml -d DGraphXML test/ParameterSpecTest/ParamView.het
Reading file /home/maeder/Hets/test/ParameterSpecTest/ParamView.het
Analyzing library ParamView
Analyzing spec s
Analyzing view v
Analyzing spec s2
Writing file: /home/maeder/Hets/test/ParameterSpecTest/ParamView.pp.xml
Writing file: test/ParameterSpecTest/ParamView.prf
Writing file: test/ParameterSpecTest/ParamView.xml

Theorems or theorem links have a status attribute that may be "open", "proven" or "outdated" (where "outdated" is not created currently).

A theorem link discharged by local inference contains a list of possibly renamed sentences that have been moved into the target node.

Note: See TracTickets for help on using tickets.