Commit 12c17094 authored by MARCHE Claude's avatar MARCHE Claude

Fixed DTD

parent b160c23d
......@@ -507,7 +507,8 @@ gallery::
xml-validate:
@for x in `find examples/ -name why3session.xml`; do \
xmllint --noout --valid $$x 2>&1 | head -1; \
xmllint --noout --dtdvalid share/why3session.dtd \
$$x 2>&1 | head -1; \
done
########
......
......@@ -117,6 +117,51 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
scheduled on Sep 2012
== New Features to announce ==
New features:
o
Bug fix:
o
== Final preparation ==
* check that nightly bench is OK
* check that "make xml-validate" is OK
* put 0.74 in file Version
* check headers
* check the file CHANGES
* manual in PDF: check that macro \todo is commented out
in ./macros.tex, and then "make doc"
* do "make distrib"
* test the distrib why3-0.73.tar.gz
* make a last commit:
- add tag 0.74 to the git repository
- do not forget to push it using git push --tags
* put on the web page
- why3-0.74.tar.gz
- standard library online, using why3doc, to http://why3.lri.fr/stdlib/
(make stdlibdoc ;
cp -r doc/stdlibdoc /users/www-perso/projets/why3/stdlib-0.74;
ln -s /users/www-perso/projets/why3/stdlib-0.74 \
/users/www-perso/projets/why3/stdlib)
- API doc, produced using ocamldoc, to http://why3.lri.fr/api/
Note: check that URL of API doc is correct in doc/api.tex line 9.
(make apidoc ;
cp -r doc/apidoc /users/www-perso/projets/why3/api-0.74;
ln -s /users/www-perso/projets/why3/api-0.74 \
/users/www-perso/projets/why3/api )
- update the main HTML page (sources are in why3-papers/www)
* produce the Why3 part of ProVal gallery ?
* Announce the distrib
- What to put in the announcement: see New Features above
* The next commit : add +git to the version in file Version
== TODOs ==
* Sortie PVS
** avec mecanisme de realization
......
<!ELEMENT why3session (prover*, file*)>
<!ATTLIST why3session name CDATA #REQUIRED>
<!ATTLIST why3session shape_version CDATA #IMPLIED>
<!ELEMENT prover EMPTY>
<!ATTLIST prover id CDATA #REQUIRED>
<!ATTLIST prover name CDATA #REQUIRED>
<!ATTLIST prover version CDATA #REQUIRED>
<!ATTLIST prover alternative CDATA #IMPLIED>
<!ELEMENT file (theory*)>
<!ATTLIST file name CDATA #REQUIRED>
......@@ -41,7 +43,7 @@
<!ATTLIST proof archived CDATA #IMPLIED>
<!ELEMENT result EMPTY>
<!ATTLIST result status (valid|invalid|unknown|timeout|failure) #REQUIRED>
<!ATTLIST result status (valid|invalid|unknown|timeout|outofmemory|failure) #REQUIRED>
<!ATTLIST result time CDATA #IMPLIED>
<!ELEMENT undone EMPTY>
......@@ -86,7 +88,8 @@
<!ATTLIST pr_pos proj CDATA #REQUIRED>
<!ATTLIST pr_pos sum CDATA #REQUIRED>
<!ELEMENT meta (meta_arg_ty*, meta_arg_ts*, meta_arg_ls*, meta_arg_pr*, meta_arg_str*, meta_arg_int*)>
<!ELEMENT meta (meta_arg_ty*, meta_arg_ts*, meta_arg_ls*,
meta_arg_pr*, meta_arg_str*, meta_arg_int*)>
<!ATTLIST meta name CDATA #REQUIRED>
<!ELEMENT meta_args_ty (ty_var|ty_app)>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment