]>
matita.cs.unibo.it Git - helm.git/log
Claudio Sacerdoti Coen [Tue, 16 Apr 2002 09:34:07 +0000 (09:34 +0000)]
* Bug fixed: applications of MutCase that are not iota-redexes were reduced
just to their head.
* More debugging enabled (to be removed when code becomes stable)
Claudio Sacerdoti Coen [Tue, 16 Apr 2002 09:16:17 +0000 (09:16 +0000)]
Invariant enforced: no Appl of another Appl.
Andrea Asperti [Tue, 16 Apr 2002 09:00:50 +0000 (09:00 +0000)]
1. CicReduction moved into CicReductionNaif
2. CicReductionMachine is the new implementation based on an
"environment machine".
You must make a sumbolic link from one implementation (.ml) to
cicReduction.ml
Andrea Asperti [Tue, 16 Apr 2002 08:41:29 +0000 (08:41 +0000)]
Replaced with a symbolic link to the actual implementation.
The symbolic link must be created after check-out.
Andrea Asperti [Tue, 16 Apr 2002 08:33:53 +0000 (08:33 +0000)]
type_of_aux' exported.
Andrea Asperti [Tue, 16 Apr 2002 08:33:19 +0000 (08:33 +0000)]
Meta implemented.
Irene Schena [Mon, 15 Apr 2002 16:17:20 +0000 (16:17 +0000)]
Modified Files:
1) mmlnotation.xsl xslt_index.txt: MathML default presentation now is
generated by mmlctop.xsl
Added Files:
1) mmlctop.xsl mmlctop2_0.xsl: link and new Igor stylesheet for MathML default
presentation
Claudio Sacerdoti Coen [Fri, 12 Apr 2002 17:16:46 +0000 (17:16 +0000)]
* New slides from Saarbrucken
* DTD changed
Stefano Zacchiroli [Fri, 12 Apr 2002 13:39:38 +0000 (13:39 +0000)]
added debian stuff and a makefile with "dist" target
Stefano Zacchiroli [Fri, 12 Apr 2002 13:39:14 +0000 (13:39 +0000)]
changed name to gdome2-xslt
Stefano Zacchiroli [Fri, 12 Apr 2002 13:38:54 +0000 (13:38 +0000)]
- added -fPIC when creating .so
- added PREFIX variable support
Stefano Zacchiroli [Fri, 12 Apr 2002 13:38:17 +0000 (13:38 +0000)]
changed package name to gdome2-xslt
Stefano Zacchiroli [Fri, 12 Apr 2002 13:37:55 +0000 (13:37 +0000)]
cma names parameterized in configure @PACKAGE@ variable
Stefano Zacchiroli [Fri, 12 Apr 2002 12:35:12 +0000 (12:35 +0000)]
-7 debian release, hopefully build also on HPPA
Stefano Zacchiroli [Fri, 12 Apr 2002 12:31:44 +0000 (12:31 +0000)]
added -fPIC option when compiling ml_gtk_mathview.o
Claudio Sacerdoti Coen [Thu, 11 Apr 2002 08:50:31 +0000 (08:50 +0000)]
New data.
Claudio Sacerdoti Coen [Wed, 10 Apr 2002 17:44:42 +0000 (17:44 +0000)]
First MOWGLI paper. Many others will follow.
Claudio Sacerdoti Coen [Wed, 10 Apr 2002 17:20:05 +0000 (17:20 +0000)]
The first MOWGLI paper. Many many others will follow.
Claudio Sacerdoti Coen [Mon, 8 Apr 2002 13:12:00 +0000 (13:12 +0000)]
During the computation of the inner-type of a LAMBDA, the grandfather
was retrieved instead of the father. Fixed.
Claudio Sacerdoti Coen [Mon, 8 Apr 2002 12:57:42 +0000 (12:57 +0000)]
* Many improvements
* Proofs are now rendered in natural language. The inner-types file is
store in /public/sacerdot/innertypes and directly retrieved from there.
We must find a better solution.
* Apply tactic now implemented. It is based on the unification stuff of
Andrea.
Claudio Sacerdoti Coen [Mon, 8 Apr 2002 12:54:19 +0000 (12:54 +0000)]
Declaration and Definition renamed to Decl and Def because
Definition was already defined in the DTD.
Claudio Sacerdoti Coen [Mon, 8 Apr 2002 12:37:18 +0000 (12:37 +0000)]
Sequent rendering improved: "=======" replaced by a single solid line
Claudio Sacerdoti Coen [Mon, 8 Apr 2002 11:05:59 +0000 (11:05 +0000)]
1) Sequent object added.
2) Current Proof and META rendering improved.
Claudio Sacerdoti Coen [Fri, 5 Apr 2002 09:37:28 +0000 (09:37 +0000)]
* Many improvements.
* Intros and Exact are now implemented.
* Inner sorts are now generated and used.
* Perforation of the proof is now implemented.
Claudio Sacerdoti Coen [Tue, 2 Apr 2002 11:53:11 +0000 (11:53 +0000)]
First commit of our future proof-assistant/proof-improver (???)
This commit is based on some un-committed changes to our libraries. So,
it won't compile out-of-the-box.
Stefano Zacchiroli [Tue, 2 Apr 2002 08:14:36 +0000 (08:14 +0000)]
Added Build-Depends on t1lib-dev
Stefano Zacchiroli [Mon, 1 Apr 2002 07:46:03 +0000 (07:46 +0000)]
Added build-depend on libgdome2-cpp-smart-dev.
Stefano Zacchiroli [Sun, 31 Mar 2002 22:34:30 +0000 (22:34 +0000)]
- added some .mli and .ml to the debian package
- added depends on libgdome2-ocaml
Luca Padovani [Sat, 30 Mar 2002 17:39:21 +0000 (17:39 +0000)]
preparing for 0.1.4
Luca Padovani [Sat, 30 Mar 2002 17:39:01 +0000 (17:39 +0000)]
added libxml/ in #includes (see libxml2 ChangeLog)
Luca Padovani [Sat, 30 Mar 2002 17:22:13 +0000 (17:22 +0000)]
error in check for xml2-config
Claudio Sacerdoti Coen [Fri, 29 Mar 2002 09:54:43 +0000 (09:54 +0000)]
gMathView.mli added
Claudio Sacerdoti Coen [Thu, 28 Mar 2002 17:03:30 +0000 (17:03 +0000)]
Electra forms added.
Claudio Sacerdoti Coen [Thu, 28 Mar 2002 14:48:47 +0000 (14:48 +0000)]
The contract is now on-line (but for an excel file still missing).
Stefano Zacchiroli [Tue, 26 Mar 2002 18:23:16 +0000 (18:23 +0000)]
- Increased debian version to 0.3.0-3
- Added build depends to latest gmetadom and gtkmathview
Claudio Sacerdoti Coen [Tue, 26 Mar 2002 16:06:23 +0000 (16:06 +0000)]
The compilation of the test is restored.
It didn't compile any more due to a different behaviour of gcc on woody.
Claudio Sacerdoti Coen [Mon, 25 Mar 2002 12:24:05 +0000 (12:24 +0000)]
Links to the version with frames fixed.
Claudio Sacerdoti Coen [Fri, 22 Mar 2002 13:53:21 +0000 (13:53 +0000)]
Rendering improved.
Claudio Sacerdoti Coen [Fri, 22 Mar 2002 13:45:53 +0000 (13:45 +0000)]
Rendering improved.
Claudio Sacerdoti Coen [Fri, 22 Mar 2002 13:26:09 +0000 (13:26 +0000)]
New MOWGLI member.
Claudio Sacerdoti Coen [Fri, 22 Mar 2002 13:25:58 +0000 (13:25 +0000)]
New data.
Claudio Sacerdoti Coen [Fri, 22 Mar 2002 13:25:19 +0000 (13:25 +0000)]
Layout improved.
Luca Padovani [Thu, 21 Mar 2002 20:44:20 +0000 (20:44 +0000)]
frames/no frame switch changed
Claudio Sacerdoti Coen [Thu, 21 Mar 2002 18:45:49 +0000 (18:45 +0000)]
Links between the versions with and without frames.
Claudio Sacerdoti Coen [Wed, 20 Mar 2002 17:39:33 +0000 (17:39 +0000)]
New data.
Claudio Sacerdoti Coen [Wed, 20 Mar 2002 15:11:43 +0000 (15:11 +0000)]
mowgli-adm mailing list created
Claudio Sacerdoti Coen [Wed, 20 Mar 2002 15:00:03 +0000 (15:00 +0000)]
New MOWGLI member.
Claudio Sacerdoti Coen [Wed, 20 Mar 2002 14:59:39 +0000 (14:59 +0000)]
* New data
* New members
Claudio Sacerdoti Coen [Wed, 20 Mar 2002 14:22:56 +0000 (14:22 +0000)]
New data.
Claudio Sacerdoti Coen [Wed, 20 Mar 2002 12:45:55 +0000 (12:45 +0000)]
MOWGLI roles considered in people position
Claudio Sacerdoti Coen [Wed, 20 Mar 2002 12:18:06 +0000 (12:18 +0000)]
* New MOWGLI members
* New: summary of the MOWGLI kick-off on-line
Claudio Sacerdoti Coen [Wed, 20 Mar 2002 10:18:47 +0000 (10:18 +0000)]
New data.
Claudio Sacerdoti Coen [Tue, 19 Mar 2002 18:53:31 +0000 (18:53 +0000)]
New: Minutes of the kick-off
Claudio Sacerdoti Coen [Tue, 19 Mar 2002 17:53:54 +0000 (17:53 +0000)]
People in the "by site" list are now sorted alphabetically.
Claudio Sacerdoti Coen [Tue, 19 Mar 2002 17:35:23 +0000 (17:35 +0000)]
* Some documents were not valid
* Project Leaders added to every package
* New data in project-management
Claudio Sacerdoti Coen [Mon, 18 Mar 2002 18:49:28 +0000 (18:49 +0000)]
* Work Package Leaders added (and rendered)
* Rendering of Work Packages improved
Stefano Zacchiroli [Fri, 15 Mar 2002 12:25:08 +0000 (12:25 +0000)]
Added build dep on libgdome2-dev
Stefano Zacchiroli [Wed, 13 Mar 2002 23:20:21 +0000 (23:20 +0000)]
Debian changes for version 0.3.0 of lablgtkmathview.
Major changes:
- split shared library package
- debian native package, diff.gz is no longer needed
Claudio Sacerdoti Coen [Wed, 13 Mar 2002 18:43:35 +0000 (18:43 +0000)]
The contract was the proposal!!!
Claudio Sacerdoti Coen [Wed, 13 Mar 2002 10:24:18 +0000 (10:24 +0000)]
Data refined.
Claudio Sacerdoti Coen [Tue, 12 Mar 2002 18:03:32 +0000 (18:03 +0000)]
Initial version.
Claudio Sacerdoti Coen [Tue, 12 Mar 2002 17:41:44 +0000 (17:41 +0000)]
* Linking was still static for native compilation.
* Automatic compilation of the test in native mode can no more be performed
because the dynamic library is always searched in the position where
it will be installed ;-(
Claudio Sacerdoti Coen [Tue, 12 Mar 2002 15:45:15 +0000 (15:45 +0000)]
Data refined.
Claudio Sacerdoti Coen [Tue, 12 Mar 2002 11:46:45 +0000 (11:46 +0000)]
More data.
Claudio Sacerdoti Coen [Tue, 12 Mar 2002 10:35:03 +0000 (10:35 +0000)]
New data.
Claudio Sacerdoti Coen [Tue, 12 Mar 2002 10:28:39 +0000 (10:28 +0000)]
New Data (operative commencement date).
Claudio Sacerdoti Coen [Tue, 12 Mar 2002 10:18:55 +0000 (10:18 +0000)]
New data.
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 18:02:34 +0000 (18:02 +0000)]
Goguadze added.
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 16:05:17 +0000 (16:05 +0000)]
New sources by Paul Libbrecht. From these sources it is possible to
produce both a nice PDF file and the PS document.
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 15:51:47 +0000 (15:51 +0000)]
Link to Paul's new MOWGLI page added.
Irene Schena [Mon, 11 Mar 2002 15:51:08 +0000 (15:51 +0000)]
Modified Files:
1) dfki.xml: added member
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 15:44:36 +0000 (15:44 +0000)]
Not well-formed XML.
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 15:36:15 +0000 (15:36 +0000)]
Paul Libbrecht added.
Irene Schena [Mon, 11 Mar 2002 14:39:53 +0000 (14:39 +0000)]
Modified Files:
1) html/Makefile html/proposal/.cvsignore xml/home.xml
xml/menu.xml xml/project.xml xml/proposal/EC-contribution.xml
xml/proposal/contribution.xml
xml/proposal/econ-scient-tech-prospects.xml
xml/proposal/innovation.xml
xml/proposal/project-components.xml
xml/proposal/project-management.xml
xml/proposal/project-objectives.xml
xml/proposal/project-planning.xml
xml/proposal/project-summary.xml xsl/project.xsl: now the proposal index is
in project.xml that is linked in the Project Menu
Removed Files:
1) xml/proposal/proposal-index.xml: now is in project.xml
Irene Schena [Mon, 11 Mar 2002 13:21:25 +0000 (13:21 +0000)]
Modified Files:
1) xml/sites/aei.xml xml/sites/dfki.xml xml/sites/nijmegen.xml
xml/sites/trusted-logic.xml xsl/site.xsl: added site members info
Irene Schena [Mon, 11 Mar 2002 12:01:51 +0000 (12:01 +0000)]
Modified Files:
1) xml/home.xml xml/proposal/EC-contribution.xml
xml/proposal/contribution.xml
xml/proposal/econ-scient-tech-prospects.xml
xml/proposal/innovation.xml
xml/proposal/project-components.xml
xml/proposal/project-management.xml
xml/proposal/project-objectives.xml
xml/proposal/project-planning.xml
xml/proposal/project-summary.xml xml/sites/dfki.xml: bugs fixed
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 11:27:38 +0000 (11:27 +0000)]
New data.
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 11:27:03 +0000 (11:27 +0000)]
Markus Moschner (DFKI) added.
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 11:21:53 +0000 (11:21 +0000)]
Markus Moschner (DFKI) added.
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 11:00:47 +0000 (11:00 +0000)]
A much better PDF file contributed by Paul Libbrecht.
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 11:00:16 +0000 (11:00 +0000)]
Link to ActiveMath added.
Irene Schena [Fri, 8 Mar 2002 16:40:51 +0000 (16:40 +0000)]
Modified Files:
1) sites/dfki.xml sites/nijmegen.xml: errors fixed
Irene Schena [Fri, 8 Mar 2002 16:15:40 +0000 (16:15 +0000)]
Modified Files:
1) asperti.xml guidi.xml padovani.xml sacerdoti.xml schena.xml: info updated
Claudio Sacerdoti Coen [Fri, 8 Mar 2002 12:19:13 +0000 (12:19 +0000)]
loadDocumentFrom* and saveDocument interface changed
Irene Schena [Fri, 8 Mar 2002 12:03:40 +0000 (12:03 +0000)]
Modified Files:
1) pert_new.png: added resolution
Claudio Sacerdoti Coen [Wed, 6 Mar 2002 18:14:53 +0000 (18:14 +0000)]
-rpath used to record the path to use to search for dynamic libraries
which are not in LD_LIBRARY_PATH. (In our case, all the dynamic libraries
of the bindings this one depends on.)
Claudio Sacerdoti Coen [Wed, 6 Mar 2002 17:20:23 +0000 (17:20 +0000)]
The .so file was not moved into the temporary installation directory.
Irene Schena [Wed, 6 Mar 2002 16:59:06 +0000 (16:59 +0000)]
Added Files:
1) NextArrow.gif PreviousArrow.gif: arrows for next and prev pages
Irene Schena [Wed, 6 Mar 2002 16:57:11 +0000 (16:57 +0000)]
Modified Files:
1) html/Makefile html/proposal/.cvsignore
xml/proposal/EC-contribution.xml xml/proposal/contribution.xml
xml/proposal/econ-scient-tech-prospects.xml
xml/proposal/innovation.xml
xml/proposal/project-management.xml
xml/proposal/project-objectives.xml
xml/proposal/project-summary.xml
xml/proposal/proposal-index.xml: added links to pages and new pages
Added Files:
1) images/gantt_new.png images/pert_new.png
xml/proposal/project-components.xml
xml/proposal/project-planning.xml: added two pages with images to the
mowgli proposal
Claudio Sacerdoti Coen [Wed, 6 Mar 2002 15:35:45 +0000 (15:35 +0000)]
Dynamic loading of C code enabled.
Irene Schena [Wed, 6 Mar 2002 14:40:16 +0000 (14:40 +0000)]
Modified Files:
1) html/.cvsignore html/Makefile xml/home.xml xml/menu.xml: new menu item for
mowgli proposal
2) xml/news.xml: error fixed
Added Files:
1) html/proposal/.cvsignore
2) xml/proposal/EC-contribution.xml
xml/proposal/contribution.xml
xml/proposal/econ-scient-tech-prospects.xml
xml/proposal/innovation.xml
xml/proposal/project-management.xml
xml/proposal/project-objectives.xml
xml/proposal/project-summary.xml : files moved in the new dir proposal/
3) xml/proposal/proposal-index.xml: index of mowgli proposal
Removed Files:
1) xml/EC-contribution.xml xml/contribution.xml
xml/econ-scient-tech-prospects.xml xml/innovation.xml
xml/project-management.xml xml/project-objectives.xml
xml/project-summary.xml
Irene Schena [Wed, 6 Mar 2002 11:27:12 +0000 (11:27 +0000)]
Modified Files:
1) link.xsl mmlctop.xsl-0.14 mmlextension.xsl mmlnotation.xsl: removed redundant namespace prefix m: of the MML xref attribute
Claudio Sacerdoti Coen [Wed, 6 Mar 2002 10:12:22 +0000 (10:12 +0000)]
* New data
* <date>s of the news are now numerical
Claudio Sacerdoti Coen [Wed, 6 Mar 2002 10:11:51 +0000 (10:11 +0000)]
Agenda detailed.
Claudio Sacerdoti Coen [Tue, 5 Mar 2002 10:52:58 +0000 (10:52 +0000)]
Date mistake.
Claudio Sacerdoti Coen [Tue, 5 Mar 2002 10:10:20 +0000 (10:10 +0000)]
Forgotten links; better link names.
Claudio Sacerdoti Coen [Tue, 5 Mar 2002 10:09:20 +0000 (10:09 +0000)]
New data (Calculemus)
Irene Schena [Mon, 4 Mar 2002 16:05:57 +0000 (16:05 +0000)]
Modified Files:
1) home/html/.cvsignore home/html/Makefile: added chapter 8 of mowgli proposal
Added Files:
1) home/xml/econ-scient-tech-prospects.xml: chapter 8 of mowgli proposal
Irene Schena [Mon, 4 Mar 2002 15:39:55 +0000 (15:39 +0000)]
Modified Files:
1) home/html/.cvsignore home/html/Makefile home/xml/home.xml: added chapters 6 e 7
mowgli proposal
Added Files:
1) home/xml/EC-contribution.xml: chapters 6 e 7 mowgli proposal
Irene Schena [Mon, 4 Mar 2002 14:50:02 +0000 (14:50 +0000)]
Added Files:
1) innovation.xml: chapter 5 mowgli proposal