]> matita.cs.unibo.it Git - helm.git/log
helm.git
19 years agoadded filtering criteria on differences between number of constants in
Stefano Zacchiroli [Fri, 22 Apr 2005 08:34:45 +0000 (08:34 +0000)]
added filtering criteria on differences between number of constants in
hypothesis and conclusion, should handle better queries on terms with
metavariables

19 years ago- added no_hyp table
Stefano Zacchiroli [Fri, 22 Apr 2005 08:30:30 +0000 (08:30 +0000)]
- added no_hyp table
- changed constants number integer type to small int
- added comments describing tables

19 years agosplit precedence level of binders: \lambda has higher precedence than others
Stefano Zacchiroli [Thu, 21 Apr 2005 12:54:31 +0000 (12:54 +0000)]
split precedence level of binders: \lambda has higher precedence than others
this is the resulting precedences scheme:
  lambda > apply > infix operators > binders

19 years agoremoved ancient indirections for gTopLevel
Stefano Zacchiroli [Thu, 21 Apr 2005 12:08:31 +0000 (12:08 +0000)]
removed ancient indirections for gTopLevel

19 years agono longer build neither mathql nor hbugs per default
Stefano Zacchiroli [Thu, 21 Apr 2005 12:08:04 +0000 (12:08 +0000)]
no longer build neither mathql nor hbugs per default

19 years agobumped copyright years
Stefano Zacchiroli [Thu, 21 Apr 2005 12:07:41 +0000 (12:07 +0000)]
bumped copyright years

19 years agoutilities for creating environment dumps
Stefano Zacchiroli [Thu, 21 Apr 2005 12:07:24 +0000 (12:07 +0000)]
utilities for creating environment dumps

19 years ago(hopefully) final decision on precedence levels:
Stefano Zacchiroli [Thu, 21 Apr 2005 12:04:32 +0000 (12:04 +0000)]
(hopefully) final decision on precedence levels:
  binder > apply > infix operators

19 years agobugfixes:
Stefano Zacchiroli [Wed, 20 Apr 2005 16:47:32 +0000 (16:47 +0000)]
bugfixes:
- reference position using MetadataTypes.*_pos so that changing the
  position prefix fixes all the references
- don't generated dummy predicates which always suceed like ("mainConcl" OR
  "inConcl") for at_most checking

19 years agochanged binding strength of some parsing entries:
Stefano Zacchiroli [Wed, 20 Apr 2005 16:12:01 +0000 (16:12 +0000)]
changed binding strength of some parsing entries:
( a > b means a binds more tightly than b)
- now: infix operators > binders > application
- previous: application > infix operators > binders

19 years agoremoved spurious debugging prints
Stefano Zacchiroli [Wed, 20 Apr 2005 08:54:29 +0000 (08:54 +0000)]
removed spurious debugging prints

19 years agohtml-escapes user given expression when filling hidden field "expression"
Stefano Zacchiroli [Wed, 20 Apr 2005 08:45:32 +0000 (08:45 +0000)]
html-escapes user given expression when filling hidden field "expression"
in this way xml/html forbidden characters like "<" are converted to "&lt;"
and doesn't crash uwobo

19 years agobugfix: opt target should build html pages too
Stefano Zacchiroli [Fri, 8 Apr 2005 16:28:18 +0000 (16:28 +0000)]
bugfix: opt target should build html pages too

19 years agoadded clickable fingers
Stefano Zacchiroli [Fri, 8 Apr 2005 15:52:16 +0000 (15:52 +0000)]
added clickable fingers

19 years agochanged logo: whelp!
Stefano Zacchiroli [Fri, 8 Apr 2005 11:47:01 +0000 (11:47 +0000)]
changed logo: whelp!

19 years agothe description file was patched
Ferruccio Guidi [Fri, 8 Apr 2005 07:51:56 +0000 (07:51 +0000)]
the description file was patched

19 years agoinitial version of the "lambda-delta" calculus including:
Ferruccio Guidi [Fri, 1 Apr 2005 11:06:01 +0000 (11:06 +0000)]
initial version of the "lambda-delta" calculus including:

- Confluence of reduction
- Generation lemma
- Thinning lemma
- Substitution lemma
- Type Correctness
- Type Uniqueness
- Subject Reduction

19 years agodebian version 0.0.5-6
Stefano Zacchiroli [Wed, 30 Mar 2005 07:23:33 +0000 (07:23 +0000)]
debian version 0.0.5-6

19 years agorebuilt against ocaml 3.08.3
Stefano Zacchiroli [Tue, 29 Mar 2005 09:41:42 +0000 (09:41 +0000)]
rebuilt against ocaml 3.08.3

19 years agodebian: rebuilt against ocaml 3.08.3
Stefano Zacchiroli [Fri, 25 Mar 2005 23:45:48 +0000 (23:45 +0000)]
debian: rebuilt against ocaml 3.08.3

19 years agoremove x_gdome_caml.c generated source on "clean"
Stefano Zacchiroli [Fri, 25 Mar 2005 23:45:33 +0000 (23:45 +0000)]
remove x_gdome_caml.c generated source on "clean"

19 years agodebian: rebuilt against ocaml 3.08.2
Stefano Zacchiroli [Fri, 25 Mar 2005 23:44:44 +0000 (23:44 +0000)]
debian: rebuilt against ocaml 3.08.2

19 years agoBug fixed in assumption_tac: a missing (lift n) when a declaration
Claudio Sacerdoti Coen [Tue, 22 Mar 2005 16:05:54 +0000 (16:05 +0000)]
Bug fixed in assumption_tac: a missing (lift n) when a declaration
x : A := t is found in the context.

19 years ago- bugfix: do not fail when query_kind is missing (e.g. on /getpage)
Stefano Zacchiroli [Wed, 16 Mar 2005 16:33:10 +0000 (16:33 +0000)]
- bugfix: do not fail when query_kind is missing (e.g. on /getpage)
- bugfix: security, no longer subject to directory traversal (!)

19 years agouser smaller font in result page
Stefano Zacchiroli [Wed, 16 Mar 2005 16:21:44 +0000 (16:21 +0000)]
user smaller font in result page

19 years ago- new pretty printing of interpretations
Stefano Zacchiroli [Wed, 16 Mar 2005 16:17:03 +0000 (16:17 +0000)]
- new pretty printing of interpretations
- bugfix: interpretations are now remembered between pages
- more coherent look and feel

19 years agomake and clean also in html/
Stefano Zacchiroli [Wed, 16 Mar 2005 16:16:06 +0000 (16:16 +0000)]
make and clean also in html/

19 years agoremoved old HTML files (tagged with "old_htmls")
Stefano Zacchiroli [Wed, 16 Mar 2005 16:15:28 +0000 (16:15 +0000)]
removed old HTML files (tagged with "old_htmls")

19 years agomoogle.html is now generated, it do not needs to be in CVS
Stefano Zacchiroli [Wed, 16 Mar 2005 15:57:25 +0000 (15:57 +0000)]
moogle.html is now generated, it do not needs to be in CVS

19 years agogenerate HTML templates using XSLT starting from a bunch of .src files
Stefano Zacchiroli [Wed, 16 Mar 2005 15:56:44 +0000 (15:56 +0000)]
generate HTML templates using XSLT starting from a bunch of .src files

19 years agolook and feel improvements
Stefano Zacchiroli [Wed, 16 Mar 2005 15:50:35 +0000 (15:50 +0000)]
look and feel improvements

19 years ago- re-enginered main moogle template, it is now aware of queries kind, summary,
Stefano Zacchiroli [Wed, 16 Mar 2005 10:23:37 +0000 (10:23 +0000)]
- re-enginered main moogle template, it is now aware of queries kind, summary,
  and results. This enable fixing of minor like feedback on the query kind in
  case of errors
- minor bug fixes: 1/0 nuisance in case of errors
- commented out advanced query selection (which do nothing)

19 years ago- handle metavariables: if at least one of them is present, then the
Stefano Zacchiroli [Tue, 15 Mar 2005 08:27:10 +0000 (08:27 +0000)]
- handle metavariables: if at least one of them is present, then the
  cardinality constraint is not enforce
- commented out debugging prints

19 years agobugfix when user query contains metas: their context should not be analyzed
Stefano Zacchiroli [Tue, 15 Mar 2005 08:21:56 +0000 (08:21 +0000)]
bugfix when user query contains metas: their context should not be analyzed
as it were in main position

19 years agoBugfix in restore_from_channel, before this fix hashtable (which has uris as
Stefano Zacchiroli [Fri, 11 Mar 2005 18:37:41 +0000 (18:37 +0000)]
Bugfix in restore_from_channel, before this fix hashtable (which has uris as
keys and pairs <objects,universe> as values) was dumped but restored as if it
have uris as keys and objects as values. That caused immediate segfaults
while trying to iterated on the restored table.

19 years agoadded support for open terms in check
Stefano Zacchiroli [Wed, 9 Mar 2005 10:24:03 +0000 (10:24 +0000)]
added support for open terms in check

19 years agosupport for terms with metas in check
Stefano Zacchiroli [Wed, 9 Mar 2005 10:22:39 +0000 (10:22 +0000)]
support for terms with metas in check

19 years agoadded choose_uri method to console, used by the interpreter to implement the
Enrico Tassi [Mon, 14 Feb 2005 15:12:24 +0000 (15:12 +0000)]
added choose_uri method to console, used by the interpreter to implement the
hint command

19 years agoAdded heuristic in the Appl case, we beta-expand only if the argument list
Enrico Tassi [Mon, 14 Feb 2005 12:06:45 +0000 (12:06 +0000)]
Added heuristic in the Appl case, we beta-expand only if the argument list
does't contain metas.

19 years agoFixed remove operation and get_obj (that now correctly searches in the
Enrico Tassi [Mon, 14 Feb 2005 09:51:39 +0000 (09:51 +0000)]
Fixed remove operation and get_obj (that now correctly searches in the
unchecked_list).

19 years agomoved a debug print so that it is executed for each phrase
Stefano Zacchiroli [Thu, 10 Feb 2005 16:12:17 +0000 (16:12 +0000)]
moved a debug print so that it is executed for each phrase

19 years agoadapted to optional comment lexer interface
Stefano Zacchiroli [Thu, 10 Feb 2005 16:06:36 +0000 (16:06 +0000)]
adapted to optional comment lexer interface

19 years agorenaming "remove_term" -> "remove_obj"
Stefano Zacchiroli [Thu, 10 Feb 2005 15:54:44 +0000 (15:54 +0000)]
renaming "remove_term" -> "remove_obj"

19 years ago- fix in intro parsing
Stefano Zacchiroli [Thu, 10 Feb 2005 15:54:00 +0000 (15:54 +0000)]
- fix in intro parsing
- avoid generating seq tactical for a 1-length sequences

19 years agofactorized tacticals separator and terminator
Stefano Zacchiroli [Thu, 10 Feb 2005 15:52:22 +0000 (15:52 +0000)]
factorized tacticals separator and terminator

19 years agoadded "unindex" to undo indexing of a single object
Stefano Zacchiroli [Thu, 10 Feb 2005 15:51:42 +0000 (15:51 +0000)]
added "unindex" to undo indexing of a single object

19 years agobugfix: method 'advance' now took in input concrete syntax since atm
Stefano Zacchiroli [Thu, 10 Feb 2005 15:45:40 +0000 (15:45 +0000)]
bugfix: method 'advance' now took in input concrete syntax since atm
pretty printing is not the inverse operation of parsing

19 years agochanged toolbar window type
Stefano Zacchiroli [Thu, 10 Feb 2005 15:44:34 +0000 (15:44 +0000)]
changed toolbar window type

19 years agobugfix: avoid executing tactic for the script twice
Stefano Zacchiroli [Thu, 10 Feb 2005 15:44:20 +0000 (15:44 +0000)]
bugfix: avoid executing tactic for the script twice

19 years agoremoved spurious dependency on Dbi_mysql
Stefano Zacchiroli [Thu, 10 Feb 2005 09:55:02 +0000 (09:55 +0000)]
removed spurious dependency on Dbi_mysql

19 years agoadded script support a la coqide
Stefano Zacchiroli [Wed, 9 Feb 2005 15:07:37 +0000 (15:07 +0000)]
added script support a la coqide

19 years ago- fixed "error loading dom error" avoiding sequent_viewer be delivered
Stefano Zacchiroli [Wed, 9 Feb 2005 15:07:22 +0000 (15:07 +0000)]
- fixed "error loading dom error" avoiding sequent_viewer be delivered
  the destroy signal when resetting the notebook
- added singleton instances of sequent_viewer and sequents_viewer

19 years agomoved lockScript to MatitaScript module
Stefano Zacchiroli [Wed, 9 Feb 2005 15:06:25 +0000 (15:06 +0000)]
moved lockScript to MatitaScript module

19 years ago0.1.0-1 entry
Stefano Zacchiroli [Tue, 8 Feb 2005 21:53:41 +0000 (21:53 +0000)]
0.1.0-1 entry

19 years agostrip debian version from META version
Stefano Zacchiroli [Tue, 8 Feb 2005 21:50:44 +0000 (21:50 +0000)]
strip debian version from META version

19 years agouse wildcard in install target so that binary objects are installed only
Stefano Zacchiroli [Tue, 8 Feb 2005 21:43:30 +0000 (21:43 +0000)]
use wildcard in install target so that binary objects are installed only
when built

19 years agoadded a missing unchecked_to_frozen (fixes a Not_found exception while
Stefano Zacchiroli [Tue, 8 Feb 2005 17:28:21 +0000 (17:28 +0000)]
added a missing unchecked_to_frozen (fixes a Not_found exception while
type checking without trust)

19 years agoat_least now supports the ownerized tables
Enrico Tassi [Tue, 8 Feb 2005 15:47:49 +0000 (15:47 +0000)]
at_least now supports the ownerized tables

19 years agoadded boxml namespace
Stefano Zacchiroli [Tue, 8 Feb 2005 15:35:52 +0000 (15:35 +0000)]
added boxml namespace

19 years ago- changed license to lgpl
Stefano Zacchiroli [Tue, 8 Feb 2005 12:16:04 +0000 (12:16 +0000)]
- changed license to lgpl
- bumped copyright
- improved ocamldoc comments

19 years agodebian changes target release 0.1.0
Stefano Zacchiroli [Tue, 8 Feb 2005 12:15:09 +0000 (12:15 +0000)]
debian changes target release 0.1.0

19 years agoincluded lgpl
Stefano Zacchiroli [Tue, 8 Feb 2005 12:14:34 +0000 (12:14 +0000)]
included lgpl

19 years agoadded TODO file
Stefano Zacchiroli [Mon, 7 Feb 2005 15:24:07 +0000 (15:24 +0000)]
added TODO file

19 years agoadded support for directory browsing in cicBrowser
Stefano Zacchiroli [Mon, 7 Feb 2005 15:23:02 +0000 (15:23 +0000)]
added support for directory browsing in cicBrowser

19 years agorebuilt
Stefano Zacchiroli [Mon, 7 Feb 2005 15:22:44 +0000 (15:22 +0000)]
rebuilt

19 years agoconnected change tactic (proof of concept)
Stefano Zacchiroli [Mon, 7 Feb 2005 15:22:37 +0000 (15:22 +0000)]
connected change tactic (proof of concept)

19 years agoremoved chosenTransformer.ml*
Enrico Tassi [Mon, 7 Feb 2005 12:07:41 +0000 (12:07 +0000)]
removed chosenTransformer.ml*

19 years agoremoved chosenTransformer.mli
Enrico Tassi [Mon, 7 Feb 2005 11:49:16 +0000 (11:49 +0000)]
removed chosenTransformer.mli

19 years agosync with Xml.pp
Enrico Tassi [Mon, 7 Feb 2005 10:25:53 +0000 (10:25 +0000)]
sync with Xml.pp

19 years agofix join on multiple tables
Stefano Zacchiroli [Fri, 4 Feb 2005 16:52:29 +0000 (16:52 +0000)]
fix join on multiple tables

19 years agofixed Gzip bug in Xml.pp
Enrico Tassi [Fri, 4 Feb 2005 16:15:44 +0000 (16:15 +0000)]
fixed Gzip bug in Xml.pp

19 years agosaves to gzip
Enrico Tassi [Fri, 4 Feb 2005 16:13:28 +0000 (16:13 +0000)]
saves to gzip

19 years agoadded library table and owner tables handling in the SQL code
Enrico Tassi [Fri, 4 Feb 2005 15:47:40 +0000 (15:47 +0000)]
added library table and owner tables handling in the SQL code

19 years agoescape exception name and arguments embedded in root element attributes
Stefano Zacchiroli [Fri, 4 Feb 2005 15:04:53 +0000 (15:04 +0000)]
escape exception name and arguments embedded in root element attributes
to avoid non well formed xml documents to be generated

19 years agobugfix: handling of local resources (not to be cached) when they are zipped,
Stefano Zacchiroli [Fri, 4 Feb 2005 15:03:58 +0000 (15:03 +0000)]
bugfix: handling of local resources (not to be cached) when they are zipped,
avoid former Sys_error exception for not existent files

19 years agochanged local_url so that it returns the local part of a file:// scheme url
Stefano Zacchiroli [Fri, 4 Feb 2005 15:03:22 +0000 (15:03 +0000)]
changed local_url so that it returns the local part of a file:// scheme url

19 years ago- removed special handling of universes (no longer needed)
Stefano Zacchiroli [Fri, 4 Feb 2005 15:02:38 +0000 (15:02 +0000)]
- removed special handling of universes (no longer needed)
- removed ancient part of commented code

19 years ago"thin" version of the configuration file (exploits default values and
Stefano Zacchiroli [Fri, 4 Feb 2005 14:03:03 +0000 (14:03 +0000)]
"thin" version of the configuration file (exploits default values and
new configuration parameters like maps_dir and cache_dir)

19 years ago- added some default values (no longer explicitely required in the
Stefano Zacchiroli [Fri, 4 Feb 2005 14:02:20 +0000 (14:02 +0000)]
- added some default values (no longer explicitely required in the
  configuration file)
- bugfix: read configuration values from the environment and not
  directly via Helm_registry

19 years agoadded gzip support to Xml
Stefano Zacchiroli [Fri, 4 Feb 2005 13:58:53 +0000 (13:58 +0000)]
added gzip support to Xml

19 years agolocate now searched bot the standard library and the owner(user) library
Enrico Tassi [Fri, 4 Feb 2005 13:02:57 +0000 (13:02 +0000)]
locate now searched bot the standard library and the owner(user) library

19 years agofix
Enrico Tassi [Fri, 4 Feb 2005 13:01:29 +0000 (13:01 +0000)]
fix

19 years agoreturn also .types uri in getalluris/
Stefano Zacchiroli [Fri, 4 Feb 2005 12:11:07 +0000 (12:11 +0000)]
return also .types uri in getalluris/

19 years agosnapshot, notably:
Stefano Zacchiroli [Fri, 4 Feb 2005 11:10:52 +0000 (11:10 +0000)]
snapshot, notably:
- even more singleton instances: disambiguator is now common to matita
  and matitac, but matita set different callbacks which uses gtk
- getter now embedded in matita (no longer use remote getter)
- use onwerization of tables

19 years agoparameterized lexer so that comment tokens could be returned or not,
Stefano Zacchiroli [Fri, 4 Feb 2005 09:30:47 +0000 (09:30 +0000)]
parameterized lexer so that comment tokens could be returned or not,
per default they are not returned

19 years agoremoved dep on mathql
Stefano Zacchiroli [Fri, 4 Feb 2005 09:29:50 +0000 (09:29 +0000)]
removed dep on mathql

19 years agorebuilt
Stefano Zacchiroli [Fri, 4 Feb 2005 09:29:03 +0000 (09:29 +0000)]
rebuilt

19 years ago- removed dependency on mathql
Stefano Zacchiroli [Fri, 4 Feb 2005 09:28:42 +0000 (09:28 +0000)]
- removed dependency on mathql
- cosmetic changes

19 years ago- added init method
Stefano Zacchiroli [Fri, 4 Feb 2005 09:28:07 +0000 (09:28 +0000)]
- added init method
- added default values for loglevel and logfile

19 years agorebuild
Stefano Zacchiroli [Fri, 4 Feb 2005 09:27:30 +0000 (09:27 +0000)]
rebuild

19 years ago- simplified environment handling:
Stefano Zacchiroli [Fri, 4 Feb 2005 09:26:59 +0000 (09:26 +0000)]
- simplified environment handling:
  * added a lot of default values
  * use maps_dir instead of dbm files file-per-file
  * use cache_dir instead of cache dirs dir-per-dir
  * servers could now either be listed in servers.txt or directly in
    configuration file

19 years agolocal_url predicate (recognize file:// urls)
Stefano Zacchiroli [Fri, 4 Feb 2005 09:24:46 +0000 (09:24 +0000)]
local_url predicate (recognize file:// urls)

19 years agodo not cache local resources (i.e. file:// urls)
Stefano Zacchiroli [Fri, 4 Feb 2005 09:24:01 +0000 (09:24 +0000)]
do not cache local resources (i.e. file:// urls)

19 years agocreate path towards dbm file
Stefano Zacchiroli [Fri, 4 Feb 2005 09:23:27 +0000 (09:23 +0000)]
create path towards dbm file

19 years agoremoved ancient mathql deps
Stefano Zacchiroli [Fri, 4 Feb 2005 09:15:40 +0000 (09:15 +0000)]
removed ancient mathql deps

19 years ago- clean no longer unregister URIs from the getter, but returns them
Stefano Zacchiroli [Fri, 4 Feb 2005 09:15:10 +0000 (09:15 +0000)]
- clean no longer unregister URIs from the getter, but returns them
- removed owner table handling

19 years agocosmetic changes
Stefano Zacchiroli [Fri, 4 Feb 2005 09:14:32 +0000 (09:14 +0000)]
cosmetic changes

19 years agotarget 0.1.0 changelog (not yet released ...)
Stefano Zacchiroli [Thu, 3 Feb 2005 22:31:35 +0000 (22:31 +0000)]
target 0.1.0 changelog (not yet released ...)

19 years agouniformed default values handling, now they are all in this module and
Stefano Zacchiroli [Thu, 3 Feb 2005 22:25:16 +0000 (22:25 +0000)]
uniformed default values handling, now they are all in this module and
consistent with optional arguments of start functions

19 years ago- added main that starts a new http_daemon given a daemon_spec (see
Stefano Zacchiroli [Thu, 3 Feb 2005 22:24:29 +0000 (22:24 +0000)]
- added main that starts a new http_daemon given a daemon_spec (see
  Http_types.daemon_spec)
- added default_spec
- deprecated start and start' in favour of main