]> matita.cs.unibo.it Git - helm.git/log
helm.git
18 years agoremoved papers that have been moved to the new "papers" repository
Stefano Zacchiroli [Mon, 6 Feb 2006 17:35:52 +0000 (17:35 +0000)]
removed papers that have been moved to the new "papers" repository

18 years agoabsolute path and factorization for matita.basedir
Stefano Zacchiroli [Mon, 6 Feb 2006 17:22:11 +0000 (17:22 +0000)]
absolute path and factorization for matita.basedir

18 years ago- changed semantics of "init": now it is idempotent
Stefano Zacchiroli [Mon, 6 Feb 2006 17:21:39 +0000 (17:21 +0000)]
- changed semantics of "init": now it is idempotent
- added support for "-v" flag printing "make" command line
- minor change: lazy discovering of whether we are ".opt" or not

18 years agouse matita.verbosity instead of matita.quiet
Stefano Zacchiroli [Mon, 6 Feb 2006 17:19:52 +0000 (17:19 +0000)]
use matita.verbosity instead of matita.quiet

18 years ago- uniformed command line handling of matitamake with that of other matita tools
Stefano Zacchiroli [Mon, 6 Feb 2006 17:19:28 +0000 (17:19 +0000)]
- uniformed command line handling of matitamake with that of other matita tools
- changed "-q" flag semantics: now it reduce the "matita.verbosity" value by 1
  unit
- added "-v" flag: it increase the "matita.verbosity" value by 1
- "matita.quiet" is no longer in use

18 years agohelp path is no longer hard coded but relative to runtime base dir
Stefano Zacchiroli [Mon, 6 Feb 2006 17:17:10 +0000 (17:17 +0000)]
help path is no longer hard coded but relative to runtime base dir

18 years agofixed tactic ids to include a "tac_" prefix
Stefano Zacchiroli [Mon, 6 Feb 2006 17:16:40 +0000 (17:16 +0000)]
fixed tactic ids to include a "tac_" prefix

18 years ago- bugfix: pass -conffile to matitamake
Stefano Zacchiroli [Mon, 6 Feb 2006 17:15:30 +0000 (17:15 +0000)]
- bugfix: pass -conffile to matitamake
- more quiet feedback during compilation of stdlib

18 years agoBasic facts about group morphisms.
Claudio Sacerdoti Coen [Mon, 6 Feb 2006 14:00:18 +0000 (14:00 +0000)]
Basic facts about group morphisms.

18 years agomoved mathql/ under software/
Stefano Zacchiroli [Mon, 6 Feb 2006 11:33:01 +0000 (11:33 +0000)]
moved mathql/ under software/

18 years agofirst sketch of the documentation (to be used by yelp)
Claudio Sacerdoti Coen [Mon, 6 Feb 2006 11:22:27 +0000 (11:22 +0000)]
first sketch of the documentation (to be used by yelp)

18 years agos/ocaml/components/ in the "tag" target
Stefano Zacchiroli [Mon, 6 Feb 2006 11:18:22 +0000 (11:18 +0000)]
s/ocaml/components/ in the "tag" target

18 years ago* groups splitted into groups and finite_groups
Claudio Sacerdoti Coen [Mon, 6 Feb 2006 10:34:27 +0000 (10:34 +0000)]
* groups splitted into groups and finite_groups
* a few lemmas added to groups

18 years agoremoved a Pcre capture that being _NON TAIL RECURSIVE_ used to cause stack_overflow...
Claudio Sacerdoti Coen [Mon, 6 Feb 2006 10:28:11 +0000 (10:28 +0000)]
removed a Pcre capture that being _NON TAIL RECURSIVE_ used to cause stack_overflow... mah...

18 years agotermine bacato.
Andrea Asperti [Mon, 6 Feb 2006 09:58:37 +0000 (09:58 +0000)]
termine bacato.

18 years agofixed usage of matita.auto_disambiguation
Andrea Asperti [Mon, 6 Feb 2006 09:40:31 +0000 (09:40 +0000)]
fixed usage of matita.auto_disambiguation

18 years agoBug?
Andrea Asperti [Mon, 6 Feb 2006 08:16:41 +0000 (08:16 +0000)]
Bug?

18 years agoFirst proof on groups completed!
Claudio Sacerdoti Coen [Fri, 3 Feb 2006 17:56:17 +0000 (17:56 +0000)]
First proof on groups completed!

18 years agofixed download links and added underlined hyperlinks
Stefano Zacchiroli [Fri, 3 Feb 2006 17:39:06 +0000 (17:39 +0000)]
fixed download links and added underlined hyperlinks

18 years agoon the fly generation of distribution configure.ac
Stefano Zacchiroli [Fri, 3 Feb 2006 17:33:46 +0000 (17:33 +0000)]
on the fly generation of distribution configure.ac

18 years agoadded bg
Enrico Tassi [Fri, 3 Feb 2006 17:29:42 +0000 (17:29 +0000)]
added bg

18 years agofix
Enrico Tassi [Fri, 3 Feb 2006 16:30:53 +0000 (16:30 +0000)]
fix

18 years agoremoved no longer needed libs link
Stefano Zacchiroli [Fri, 3 Feb 2006 16:15:32 +0000 (16:15 +0000)]
removed no longer needed libs link

18 years agoAdded abstract.
Andrea Asperti [Fri, 3 Feb 2006 15:58:18 +0000 (15:58 +0000)]
Added abstract.

18 years agoported to the new svn architecture
Stefano Zacchiroli [Fri, 3 Feb 2006 15:45:12 +0000 (15:45 +0000)]
ported to the new svn architecture

18 years ago- no longer need to dynamically discover if the components dir is libs/ or
Stefano Zacchiroli [Fri, 3 Feb 2006 15:44:40 +0000 (15:44 +0000)]
- no longer need to dynamically discover if the components dir is libs/ or
  ocaml/: now it is components/(!)
- reverted default settings to the devel ones (debugging on, runtime dir=`pwd`,
  ...)

18 years agomoved (dummy) dist stuff into software/matita/
Stefano Zacchiroli [Fri, 3 Feb 2006 15:36:53 +0000 (15:36 +0000)]
moved (dummy) dist stuff into software/matita/

18 years agomoved toplevel makefile to sfotware/
Stefano Zacchiroli [Fri, 3 Feb 2006 15:35:54 +0000 (15:35 +0000)]
moved toplevel makefile to sfotware/

18 years ago- renamed ocaml/ to components/
Stefano Zacchiroli [Fri, 3 Feb 2006 15:32:38 +0000 (15:32 +0000)]
- renamed ocaml/ to components/
- moved components/ and matita/ below software/

18 years agoremoved no longer used METAs
Stefano Zacchiroli [Fri, 3 Feb 2006 15:22:21 +0000 (15:22 +0000)]
removed no longer used METAs

18 years agodo not delete Makefile and Makefile.common on distclean since they are no
Stefano Zacchiroli [Fri, 3 Feb 2006 15:19:37 +0000 (15:19 +0000)]
do not delete Makefile and Makefile.common on distclean since they are no
longer generated at configure time

18 years agomade "dtd_dir" optional, is needed only by the web server, not by matita
Stefano Zacchiroli [Fri, 3 Feb 2006 15:15:33 +0000 (15:15 +0000)]
made "dtd_dir" optional, is needed only by the web server, not by matita

18 years agoadded build time configuration of the whole components/ dir
Stefano Zacchiroli [Fri, 3 Feb 2006 15:14:49 +0000 (15:14 +0000)]
added build time configuration of the whole components/ dir

18 years agobugfix: mkdir now works also for realtive directories
Stefano Zacchiroli [Fri, 3 Feb 2006 15:14:27 +0000 (15:14 +0000)]
bugfix: mkdir now works also for realtive directories

18 years agorelease snapshot
Stefano Zacchiroli [Fri, 3 Feb 2006 15:13:40 +0000 (15:13 +0000)]
release snapshot
- split of multiple matita conffiles (users vs developers)
- removed no longer needed keys in conffiles
- commented conffiles entries
- made matitaInit.ml more like other matita tools (still a lot to do ...)
- save .xml debugging files only if debug is enabled
- ...

18 years agorelease snapshot
Stefano Zacchiroli [Fri, 3 Feb 2006 15:12:29 +0000 (15:12 +0000)]
release snapshot

18 years agosnapshot
Andrea Asperti [Fri, 3 Feb 2006 15:08:45 +0000 (15:08 +0000)]
snapshot

18 years agoModified lambda and explicit substitutions.
Andrea Asperti [Fri, 3 Feb 2006 15:08:24 +0000 (15:08 +0000)]
Modified lambda and explicit substitutions.

18 years agocosmetic fix
Stefano Zacchiroli [Fri, 3 Feb 2006 12:21:32 +0000 (12:21 +0000)]
cosmetic fix

18 years agoadded DBHOST & co ...
Stefano Zacchiroli [Fri, 3 Feb 2006 11:07:14 +0000 (11:07 +0000)]
added DBHOST & co ...

18 years agodefault of auto_disambiguation set to true
Stefano Zacchiroli [Fri, 3 Feb 2006 10:07:38 +0000 (10:07 +0000)]
default of auto_disambiguation set to true

18 years agosvn:ignore updated
Claudio Sacerdoti Coen [Fri, 3 Feb 2006 09:57:01 +0000 (09:57 +0000)]
svn:ignore updated

18 years ago- moved images in images/
Stefano Zacchiroli [Thu, 2 Feb 2006 23:02:58 +0000 (23:02 +0000)]
- moved images in images/
- now all pages are valid xhtml 1.0 strict

18 years agouse server-side include
Stefano Zacchiroli [Thu, 2 Feb 2006 22:50:31 +0000 (22:50 +0000)]
use server-side include

18 years agoadded images and links for validation
Stefano Zacchiroli [Thu, 2 Feb 2006 22:30:27 +0000 (22:30 +0000)]
added images and links for validation

18 years agofix
Enrico Tassi [Thu, 2 Feb 2006 22:24:00 +0000 (22:24 +0000)]
fix

18 years agofix
Enrico Tassi [Thu, 2 Feb 2006 21:50:22 +0000 (21:50 +0000)]
fix

18 years agofix
Enrico Tassi [Thu, 2 Feb 2006 21:41:22 +0000 (21:41 +0000)]
fix

18 years agoa further step toward releasable Makefile
Stefano Zacchiroli [Thu, 2 Feb 2006 19:01:23 +0000 (19:01 +0000)]
a further step toward releasable Makefile

18 years agoSome more work...
Claudio Sacerdoti Coen [Thu, 2 Feb 2006 19:00:34 +0000 (19:00 +0000)]
Some more work...

18 years agoreorganization continues ...
Stefano Zacchiroli [Thu, 2 Feb 2006 18:57:10 +0000 (18:57 +0000)]
reorganization continues ...

18 years ago(dis)organized web stuff
Stefano Zacchiroli [Thu, 2 Feb 2006 18:49:29 +0000 (18:49 +0000)]
(dis)organized web stuff

18 years agodaemons tamed
Stefano Zacchiroli [Thu, 2 Feb 2006 18:42:41 +0000 (18:42 +0000)]
daemons tamed

18 years agodir reorganization
Stefano Zacchiroli [Thu, 2 Feb 2006 18:20:44 +0000 (18:20 +0000)]
dir reorganization

18 years agomoved some old stuff to the history
Stefano Zacchiroli [Thu, 2 Feb 2006 18:11:00 +0000 (18:11 +0000)]
moved some old stuff to the history

18 years agoremoved "tilde_expand" hack: for the moment it is not needed (we can use $HOME)
Stefano Zacchiroli [Thu, 2 Feb 2006 16:22:23 +0000 (16:22 +0000)]
removed "tilde_expand" hack: for the moment it is not needed (we can use $HOME)
if it will be needed in the future it should be implemented (properly) in the
registry itself

18 years agoremoved no longer used coq_notation_script from API
Stefano Zacchiroli [Thu, 2 Feb 2006 16:19:01 +0000 (16:19 +0000)]
removed no longer used coq_notation_script from API

18 years agoadded fallback to environment variables when a key is not found neither in
Stefano Zacchiroli [Thu, 2 Feb 2006 16:17:55 +0000 (16:17 +0000)]
added fallback to environment variables when a key is not found neither in
the XML nor in the mangled name
setting something like:
  <key name="foo">$(HOME)</key>
now works as expected

18 years agorelease work snapshot ...
Stefano Zacchiroli [Thu, 2 Feb 2006 15:41:50 +0000 (15:41 +0000)]
release work snapshot ...

18 years agoadded meta targets all, opt, ...
Stefano Zacchiroli [Thu, 2 Feb 2006 14:31:25 +0000 (14:31 +0000)]
added meta targets all, opt, ...

18 years agosnapshot
Stefano Zacchiroli [Thu, 2 Feb 2006 14:07:49 +0000 (14:07 +0000)]
snapshot

18 years agono longer ignore Makefile.defs
Stefano Zacchiroli [Thu, 2 Feb 2006 14:05:19 +0000 (14:05 +0000)]
no longer ignore Makefile.defs

18 years agono more multiple configure/Makefile, just one for both ocaml/ and matita/
Stefano Zacchiroli [Thu, 2 Feb 2006 14:02:18 +0000 (14:02 +0000)]
no more multiple configure/Makefile, just one for both ocaml/ and matita/

18 years agoworking on the release ... la la la
Stefano Zacchiroli [Thu, 2 Feb 2006 13:36:36 +0000 (13:36 +0000)]
working on the release ... la la la

18 years agomore style fixes
Enrico Tassi [Thu, 2 Feb 2006 11:44:44 +0000 (11:44 +0000)]
more style fixes

18 years agoNo longer valid comment removed.
Claudio Sacerdoti Coen [Thu, 2 Feb 2006 10:59:05 +0000 (10:59 +0000)]
No longer valid comment removed.

18 years ago- "ocaml/" -> "libs/" in the distribution
Stefano Zacchiroli [Thu, 2 Feb 2006 10:57:27 +0000 (10:57 +0000)]
- "ocaml/" -> "libs/" in the distribution
- fresh copy of configure.ac

18 years agorelease snapshot ...
Stefano Zacchiroli [Thu, 2 Feb 2006 10:53:51 +0000 (10:53 +0000)]
release snapshot ...

18 years agoported to the IEEE latex8 style
Enrico Tassi [Thu, 2 Feb 2006 10:49:28 +0000 (10:49 +0000)]
ported to the IEEE latex8 style

18 years agoadded (placeholder) distribution stuff for matita
Stefano Zacchiroli [Thu, 2 Feb 2006 10:47:22 +0000 (10:47 +0000)]
added (placeholder) distribution stuff for matita

18 years agoremoved obsolete library installation dir setting
Stefano Zacchiroli [Thu, 2 Feb 2006 10:37:52 +0000 (10:37 +0000)]
removed obsolete library installation dir setting

18 years agomoved dot stuff to STATS/
Stefano Zacchiroli [Thu, 2 Feb 2006 10:35:13 +0000 (10:35 +0000)]
moved dot stuff to STATS/

18 years agomoved mathql metas to mathql/
Stefano Zacchiroli [Thu, 2 Feb 2006 10:16:04 +0000 (10:16 +0000)]
moved mathql metas to mathql/

18 years agomoved mathql side by side with ocaml/
Stefano Zacchiroli [Thu, 2 Feb 2006 10:13:14 +0000 (10:13 +0000)]
moved mathql side by side with ocaml/

18 years agoline breaking
Stefano Zacchiroli [Wed, 1 Feb 2006 23:12:00 +0000 (23:12 +0000)]
line breaking

18 years agonear to the final version ...
Stefano Zacchiroli [Wed, 1 Feb 2006 23:09:56 +0000 (23:09 +0000)]
near to the final version ...

18 years agoreview on csc's latest additions
Stefano Zacchiroli [Wed, 1 Feb 2006 22:56:18 +0000 (22:56 +0000)]
review on csc's latest additions

18 years agoadded links to svn tarballs
Enrico Tassi [Wed, 1 Feb 2006 22:42:23 +0000 (22:42 +0000)]
added links to svn tarballs

18 years agoCloser to the proof of the pigeonhole principle... that is already in the
Claudio Sacerdoti Coen [Wed, 1 Feb 2006 18:48:12 +0000 (18:48 +0000)]
Closer to the proof of the pigeonhole principle... that is already in the
library as a theorem over permutations :-(

18 years agoBug fixed in generalization: the goals opened by lazy parsing of the
Claudio Sacerdoti Coen [Wed, 1 Feb 2006 18:35:29 +0000 (18:35 +0000)]
Bug fixed in generalization: the goals opened by lazy parsing of the
generalization argument were not reported correctly. This fix is not
100% correct, but it will do for now. The best solution would be to
add a new tactic to modify the metasenv and to make the status type
private.

18 years agoAbstract and conclusions.
Claudio Sacerdoti Coen [Wed, 1 Feb 2006 17:57:43 +0000 (17:57 +0000)]
Abstract and conclusions.

18 years agoSnapshot
Andrea Asperti [Wed, 1 Feb 2006 16:56:15 +0000 (16:56 +0000)]
Snapshot

18 years agoSnapshot
Andrea Asperti [Wed, 1 Feb 2006 16:26:04 +0000 (16:26 +0000)]
Snapshot

18 years agoline breaking
Stefano Zacchiroli [Wed, 1 Feb 2006 09:18:14 +0000 (09:18 +0000)]
line breaking

18 years agospell checking
Stefano Zacchiroli [Wed, 1 Feb 2006 09:04:13 +0000 (09:04 +0000)]
spell checking

18 years agoPigeonhole proof restructured.
Claudio Sacerdoti Coen [Tue, 31 Jan 2006 18:23:43 +0000 (18:23 +0000)]
Pigeonhole proof restructured.

18 years agoSome more work on the proof of the pigeonhole principle.
Claudio Sacerdoti Coen [Tue, 31 Jan 2006 18:00:08 +0000 (18:00 +0000)]
Some more work on the proof of the pigeonhole principle.
Really tougher than expected.

18 years agoBug fixed in generalize: a status was generated with an old metasenv.
Claudio Sacerdoti Coen [Tue, 31 Jan 2006 17:56:28 +0000 (17:56 +0000)]
Bug fixed in generalize: a status was generated with an old metasenv.

18 years agoadded fix for marangon
Enrico Tassi [Tue, 31 Jan 2006 16:28:05 +0000 (16:28 +0000)]
added fix for marangon

18 years agouse math mode when referencing terms from a \sequent environment
Stefano Zacchiroli [Tue, 31 Jan 2006 16:07:04 +0000 (16:07 +0000)]
use math mode when referencing terms from a \sequent environment

18 years agocommunity review, solved a couple of TODO
Claudio Sacerdoti Coen [Tue, 31 Jan 2006 15:50:06 +0000 (15:50 +0000)]
community review, solved a couple of TODO

18 years ago/me finished reviewing ...
Stefano Zacchiroli [Tue, 31 Jan 2006 13:29:40 +0000 (13:29 +0000)]
/me finished reviewing ...

18 years ago/me reviewed section 4
Stefano Zacchiroli [Tue, 31 Jan 2006 13:25:54 +0000 (13:25 +0000)]
/me reviewed section 4

18 years agofixed
Andrea Asperti [Tue, 31 Jan 2006 12:33:47 +0000 (12:33 +0000)]
fixed

18 years agofixed ocamldep command line
Andrea Asperti [Tue, 31 Jan 2006 12:32:39 +0000 (12:32 +0000)]
fixed ocamldep command line

18 years ago/me reviewed automation subsection
Stefano Zacchiroli [Tue, 31 Jan 2006 12:19:16 +0000 (12:19 +0000)]
/me reviewed automation subsection

18 years agofix
Enrico Tassi [Tue, 31 Jan 2006 12:14:00 +0000 (12:14 +0000)]
fix

18 years agofixed some depends
Enrico Tassi [Tue, 31 Jan 2006 12:09:46 +0000 (12:09 +0000)]
fixed some depends

18 years agoBug fixed: metasenv used in place of metasenv' during rewriting in an
Claudio Sacerdoti Coen [Tue, 31 Jan 2006 10:59:09 +0000 (10:59 +0000)]
Bug fixed: metasenv used in place of metasenv' during rewriting in an
hypothesis.

18 years ago/me reviewed section 3, here I go ...
Stefano Zacchiroli [Tue, 31 Jan 2006 10:55:09 +0000 (10:55 +0000)]
/me reviewed section 3, here I go ...