]> matita.cs.unibo.it Git - helm.git/log
helm.git
20 years ago* added .cc program (and equivalent .xsl stylesheet) for collecting
Luca Padovani [Mon, 8 Nov 2004 21:04:12 +0000 (21:04 +0000)]
* added .cc program (and equivalent .xsl stylesheet) for collecting
  statistics about XML files

20 years agoFirst draft (introduction).
Andrea Asperti [Mon, 8 Nov 2004 12:27:44 +0000 (12:27 +0000)]
First draft (introduction).

20 years ago...
Claudio Sacerdoti Coen [Mon, 8 Nov 2004 11:46:56 +0000 (11:46 +0000)]
...

20 years agofilled toolbar and implemented buttons behaviours
Stefano Zacchiroli [Fri, 5 Nov 2004 11:06:46 +0000 (11:06 +0000)]
filled toolbar and implemented buttons behaviours

20 years agoported to new cut and letin "API"
Stefano Zacchiroli [Fri, 5 Nov 2004 11:03:43 +0000 (11:03 +0000)]
ported to new cut and letin "API"

20 years ago- added Tactics module as a common point where tactics could be accessed
Stefano Zacchiroli [Fri, 5 Nov 2004 11:03:01 +0000 (11:03 +0000)]
- added Tactics module as a common point where tactics could be accessed

20 years agoAuto moved to a new file autoTactic.ml
Andrea Asperti [Thu, 4 Nov 2004 10:24:59 +0000 (10:24 +0000)]
Auto moved to a new file autoTactic.ml
Added a hastbl of duplicates in the library (currently filtered by
hint).

20 years agoNew version(s) of hint. One more stable (hint) and one more experimental
Andrea Asperti [Thu, 4 Nov 2004 10:22:18 +0000 (10:22 +0000)]
New version(s) of hint. One more stable (hint) and one more experimental
experimental_hint. The latter uses apply_verbose, since it needs to
get back the subproof of the goal, usually not returned by tactics.

20 years agoAdded a new boolean parameter "facts" (default=false) to most of the
Andrea Asperti [Thu, 4 Nov 2004 10:15:10 +0000 (10:15 +0000)]
Added a new boolean parameter "facts" (default=false) to most of the
methods. The idea is that when facts=true search should be restricted
to facts (theorems without hypothesis). To be used at the maximum
depth of automatic tactcis.

20 years agoPorting to the new version of auto.
Andrea Asperti [Thu, 4 Nov 2004 10:10:52 +0000 (10:10 +0000)]
Porting to the new version of auto.

20 years agosnapshot (notably: ported to mysql instead of dbi)
Stefano Zacchiroli [Wed, 3 Nov 2004 16:39:22 +0000 (16:39 +0000)]
snapshot (notably: ported to mysql instead of dbi)

20 years agono longer use Dbi module but directly use Mysql module since it's 13
Stefano Zacchiroli [Wed, 3 Nov 2004 16:31:43 +0000 (16:31 +0000)]
no longer use Dbi module but directly use Mysql module since it's 13
times faster

20 years agoadded Auto parsing
Stefano Zacchiroli [Wed, 3 Nov 2004 14:31:22 +0000 (14:31 +0000)]
added Auto parsing

20 years agoadded Auto and Hint tactic
Stefano Zacchiroli [Wed, 3 Nov 2004 14:27:55 +0000 (14:27 +0000)]
added Auto and Hint tactic

20 years ago* substitution are not rendered by default, an action is generated
Luca Padovani [Tue, 2 Nov 2004 14:29:11 +0000 (14:29 +0000)]
* substitution are not rendered by default, an action is generated

20 years agorenamed Http_client to Http_user_agent to avoid clashes with Gerd's
Stefano Zacchiroli [Tue, 2 Nov 2004 11:46:34 +0000 (11:46 +0000)]
renamed Http_client to Http_user_agent to avoid clashes with Gerd's
netclient since both Netclient and ocaml-http are used, believe it or
not, by xmlrpc

20 years agoignore typecheck_uri{,.opt}
Stefano Zacchiroli [Fri, 29 Oct 2004 12:22:30 +0000 (12:22 +0000)]
ignore typecheck_uri{,.opt}

20 years agoadded test script for typechecking URIs given on STDIN
Stefano Zacchiroli [Fri, 29 Oct 2004 12:21:39 +0000 (12:21 +0000)]
added test script for typechecking URIs given on STDIN

20 years ago- equality test on terms before trying convertibility now first tries
Stefano Zacchiroli [Fri, 29 Oct 2004 08:31:44 +0000 (08:31 +0000)]
- equality test on terms before trying convertibility now first tries
  phyisical equality between terms and then fallback to structural
  equality (same behaviour of ocaml < 3.08)
- changed behaviour of are_convertible. Before this change: equality was
  first tried on terms (as above) then, in case of failure, equality
  between weak head reduced terms was tried. Now weak head reduction is
  always performed. This change is motivated by the convertibility
  between "sin x" and "cos x" (no one was able to see the end of this
  test case). Now this test case completes almost immediately and
  regression test type checking the whole standard library does not
  shown any sensible slow down

20 years agosnapshot, notably:
Stefano Zacchiroli [Wed, 27 Oct 2004 11:50:26 +0000 (11:50 +0000)]
snapshot, notably:
- ported to Dbi disambiguation
- started implementation of coqide-like script window

20 years agoBug fixing.
Andrea Asperti [Wed, 27 Oct 2004 10:03:41 +0000 (10:03 +0000)]
Bug fixing.

20 years agobugfix: implemented interactive_user_uri_choice (trivial non-"advanced"
Stefano Zacchiroli [Tue, 26 Oct 2004 12:44:13 +0000 (12:44 +0000)]
bugfix: implemented interactive_user_uri_choice (trivial non-"advanced"
implementation: filter out variables)

20 years agoported to latest ocaml-http
Stefano Zacchiroli [Mon, 25 Oct 2004 22:16:56 +0000 (22:16 +0000)]
ported to latest ocaml-http

20 years agoimplemented pagination
Stefano Zacchiroli [Mon, 25 Oct 2004 22:14:13 +0000 (22:14 +0000)]
implemented pagination

20 years agorebuilt
Stefano Zacchiroli [Mon, 25 Oct 2004 22:13:52 +0000 (22:13 +0000)]
rebuilt

20 years ago- bugfix use disambiguator metasenv for initial proof status in hint
Stefano Zacchiroli [Mon, 25 Oct 2004 15:27:08 +0000 (15:27 +0000)]
- bugfix use disambiguator metasenv for initial proof status in hint
- use configuration file from /etc
- catch Chat_unfinished
- removed ancient debugging messages

20 years agoadded CSS information for (forthcoming) bottom bar
Stefano Zacchiroli [Mon, 25 Oct 2004 15:26:20 +0000 (15:26 +0000)]
added CSS information for (forthcoming) bottom bar

20 years agosort hint's result accordingly to the "least goal left first" principle
Stefano Zacchiroli [Mon, 25 Oct 2004 14:39:44 +0000 (14:39 +0000)]
sort hint's result accordingly to the "least goal left first" principle

20 years agobugfix in cmatch constants_no now consider also the number of types of
Stefano Zacchiroli [Mon, 25 Oct 2004 14:33:17 +0000 (14:33 +0000)]
bugfix in cmatch constants_no now consider also the number of types of
main

20 years ago- added var selection boolean to locate
Stefano Zacchiroli [Mon, 25 Oct 2004 12:50:46 +0000 (12:50 +0000)]
- added var selection boolean to locate
- added cardinality constraints checking to match_term

20 years agoadded vars selection boolean on locate
Stefano Zacchiroli [Mon, 25 Oct 2004 12:49:27 +0000 (12:49 +0000)]
added vars selection boolean on locate

20 years ago- reimplemented basic features using the helm-metadata library instead
Stefano Zacchiroli [Mon, 25 Oct 2004 12:48:58 +0000 (12:48 +0000)]
- reimplemented basic features using the helm-metadata library instead
  of MathQL. Previous version has been tagged "moogle_mathql"

20 years agoimplemented elim query
Andrea Asperti [Fri, 22 Oct 2004 14:50:55 +0000 (14:50 +0000)]
implemented elim query

20 years agoadded Hint "tactic"
Stefano Zacchiroli [Fri, 22 Oct 2004 13:03:07 +0000 (13:03 +0000)]
added Hint "tactic"

20 years agobugfix: handle overflow in powerset cardinality
Andrea Asperti [Fri, 22 Oct 2004 13:01:06 +0000 (13:01 +0000)]
bugfix: handle overflow in powerset cardinality

20 years agono longer builds by default tex_ and cic_textual_parser
Stefano Zacchiroli [Fri, 22 Oct 2004 12:57:07 +0000 (12:57 +0000)]
no longer builds by default tex_ and cic_textual_parser

20 years ago- reimplemented tacticChaser and friends in term of Metadata module and friends
Stefano Zacchiroli [Fri, 22 Oct 2004 12:56:40 +0000 (12:56 +0000)]
- reimplemented tacticChaser and friends in term of Metadata module and friends

20 years ago- support also DBI handle
Stefano Zacchiroli [Fri, 22 Oct 2004 12:55:40 +0000 (12:55 +0000)]
- support also DBI handle
- no longer use MQueryMisc

20 years agono longer build oldDisambiguate
Stefano Zacchiroli [Fri, 22 Oct 2004 12:55:16 +0000 (12:55 +0000)]
no longer build oldDisambiguate

20 years agouses DBI handle
Stefano Zacchiroli [Fri, 22 Oct 2004 12:55:01 +0000 (12:55 +0000)]
uses DBI handle

20 years ago- disambiguation now needs DBI handle
Stefano Zacchiroli [Fri, 22 Oct 2004 12:54:46 +0000 (12:54 +0000)]
- disambiguation now needs DBI handle
- no longer build by default old cic_textual_parser

20 years agoauto needs DBI handle
Stefano Zacchiroli [Fri, 22 Oct 2004 12:54:07 +0000 (12:54 +0000)]
auto needs DBI handle

20 years agotemporary: for the moment we need both MQI handle and DBI handle
Stefano Zacchiroli [Fri, 22 Oct 2004 12:53:44 +0000 (12:53 +0000)]
temporary: for the moment we need both MQI handle and DBI handle

20 years agoported to Dbi-disambiguation
Stefano Zacchiroli [Fri, 22 Oct 2004 12:53:07 +0000 (12:53 +0000)]
ported to Dbi-disambiguation

20 years agoignore boolean returned by saveDocument
Stefano Zacchiroli [Fri, 22 Oct 2004 12:52:35 +0000 (12:52 +0000)]
ignore boolean returned by saveDocument

20 years ago- added (hack) apply_tac_verbose (for auto)
Andrea Asperti [Fri, 22 Oct 2004 12:48:31 +0000 (12:48 +0000)]
- added (hack) apply_tac_verbose (for auto)
- ported to typed explicit subst

20 years ago- changed metadata type so that positions contains depth
Stefano Zacchiroli [Fri, 22 Oct 2004 12:40:58 +0000 (12:40 +0000)]
- changed metadata type so that positions contains depth
- introduced constraints (vs metadata)
- positions no longer hard coded (so that both short and long names are
  supported)
- added "where" parameter so that matching could be perfomed either on
  conclusion only or on the whole statement

20 years agoremoved reference to MQueryMisc
Stefano Zacchiroli [Fri, 22 Oct 2004 12:38:49 +0000 (12:38 +0000)]
removed reference to MQueryMisc

20 years ago- removed MQueryMisc. Ratio: it was used only for transformation uri -> term.
Stefano Zacchiroli [Fri, 22 Oct 2004 12:38:30 +0000 (12:38 +0000)]
- removed MQueryMisc. Ratio: it was used only for transformation uri -> term.
  The same feature is now available directly in CicUtil without the need
  of cic_textual_parser URIs

20 years ago- no longer depends on MQueryMisc for term_of_uri
Stefano Zacchiroli [Fri, 22 Oct 2004 12:36:53 +0000 (12:36 +0000)]
- no longer depends on MQueryMisc for term_of_uri
- disambiguation now uses MetadataQuery instead of MathQL

20 years agono longer depends on MQueryMisc
Stefano Zacchiroli [Fri, 22 Oct 2004 12:35:15 +0000 (12:35 +0000)]
no longer depends on MQueryMisc

20 years ago- ported to new getter API
Stefano Zacchiroli [Fri, 22 Oct 2004 12:34:30 +0000 (12:34 +0000)]
- ported to new getter API
- implemented remove_term

20 years agoported to typed explicit subst
Andrea Asperti [Fri, 22 Oct 2004 12:30:16 +0000 (12:30 +0000)]
ported to typed explicit subst

20 years agoremoved dependency on cic_textual_parser where this dep was used only
Stefano Zacchiroli [Fri, 22 Oct 2004 12:27:46 +0000 (12:27 +0000)]
removed dependency on cic_textual_parser where this dep was used only
for term_of_uri, now in CicUtil

20 years agodescribe exception raised by term_of_uri
Stefano Zacchiroli [Fri, 22 Oct 2004 12:25:34 +0000 (12:25 +0000)]
describe exception raised by term_of_uri

20 years agoremoved old function term_of_uri (now in CicUtil)
Stefano Zacchiroli [Fri, 22 Oct 2004 12:25:12 +0000 (12:25 +0000)]
removed old function term_of_uri (now in CicUtil)

20 years agobe more quiet (removed debugging prints)
Andrea Asperti [Fri, 22 Oct 2004 12:21:32 +0000 (12:21 +0000)]
be more quiet (removed debugging prints)

20 years agoported to typed explicit subst
Andrea Asperti [Fri, 22 Oct 2004 12:18:22 +0000 (12:18 +0000)]
ported to typed explicit subst

20 years agorebuilt
Andrea Asperti [Fri, 22 Oct 2004 12:18:16 +0000 (12:18 +0000)]
rebuilt

20 years ago- ported to typed explicit subst
Andrea Asperti [Fri, 22 Oct 2004 12:16:22 +0000 (12:16 +0000)]
- ported to typed explicit subst
- beta expansion in the case of Appl commented, waiting for a better
  solution

20 years ago- ported to typed explicit subst
Andrea Asperti [Fri, 22 Oct 2004 12:07:14 +0000 (12:07 +0000)]
- ported to typed explicit subst

20 years ago- ported to typed explicit substitutions
Andrea Asperti [Fri, 22 Oct 2004 12:05:26 +0000 (12:05 +0000)]
- ported to typed explicit substitutions
  (this implies that kernel wrappers which used to handle substitutions
  are vanished)

20 years ago- ported to typed explicit substitutions
Andrea Asperti [Fri, 22 Oct 2004 11:58:20 +0000 (11:58 +0000)]
- ported to typed explicit substitutions

20 years agocleanup temp files on parser failure
Andrea Asperti [Fri, 22 Oct 2004 11:57:18 +0000 (11:57 +0000)]
cleanup temp files on parser failure

20 years ago- reimplemented meta_closed in non CPS way (faster!)
Andrea Asperti [Fri, 22 Oct 2004 11:55:41 +0000 (11:55 +0000)]
- reimplemented meta_closed in non CPS way (faster!)
- ported to typed explicit substitutions

20 years agoadded type to explicit substitutions
Andrea Asperti [Fri, 22 Oct 2004 11:54:57 +0000 (11:54 +0000)]
added type to explicit substitutions

20 years ago- use CicUtil.term_of_uri instead of deprecated HelmLibrayObjects
Stefano Zacchiroli [Fri, 22 Oct 2004 09:54:49 +0000 (09:54 +0000)]
- use CicUtil.term_of_uri instead of deprecated HelmLibrayObjects
  similar function
- reverted to old syntax for binders (e.g. \forall x,y:nat.x=y)
- use ";;" as phrases terminator

20 years ago- bugfix: sequences like ".(" are now lexed, correctly, as
Stefano Zacchiroli [Fri, 22 Oct 2004 09:53:51 +0000 (09:53 +0000)]
- bugfix: sequences like ".(" are now lexed, correctly, as
  [ SYMBOL "."; PAREN "("] instead of [ SYMBOL ".(" ]

20 years agouse helm-cic_textual_parser2 findlib package when building tests
Stefano Zacchiroli [Fri, 22 Oct 2004 09:52:36 +0000 (09:52 +0000)]
use helm-cic_textual_parser2 findlib package when building tests

20 years agoadded dep on helm-metadata
Stefano Zacchiroli [Thu, 21 Oct 2004 15:56:12 +0000 (15:56 +0000)]
added dep on helm-metadata

20 years agobugfix: use only baseuri in uri part of MutInd and MutConstruct
Stefano Zacchiroli [Thu, 21 Oct 2004 15:53:25 +0000 (15:53 +0000)]
bugfix: use only baseuri in uri part of MutInd and MutConstruct

20 years agouse latest Http_getter module API
Stefano Zacchiroli [Thu, 21 Oct 2004 13:20:11 +0000 (13:20 +0000)]
use latest Http_getter module API

20 years ago- API change (renamed some exceptions)
Stefano Zacchiroli [Thu, 21 Oct 2004 13:16:58 +0000 (13:16 +0000)]
- API change (renamed some exceptions)
- ported to the latest PXP version

20 years agoadded reference to MetadataQuery (now it builds properly)
Stefano Zacchiroli [Thu, 21 Oct 2004 08:14:40 +0000 (08:14 +0000)]
added reference to MetadataQuery (now it builds properly)

20 years agoimplemented in place old Filter_auto filtering
Stefano Zacchiroli [Thu, 21 Oct 2004 08:14:13 +0000 (08:14 +0000)]
implemented in place old Filter_auto filtering

20 years agofixed a buggy pattern matching
Stefano Zacchiroli [Thu, 21 Oct 2004 08:13:49 +0000 (08:13 +0000)]
fixed a buggy pattern matching

20 years ago- split metadata type in metadata and constraints. Metadata are computed
Stefano Zacchiroli [Thu, 21 Oct 2004 07:25:27 +0000 (07:25 +0000)]
- split metadata type in metadata and constraints. Metadata are computed
  from cic objects while constraints are used to query the database

20 years ago- removed cic_cache and cic_annotations_cache
Andrea Asperti [Wed, 20 Oct 2004 11:03:59 +0000 (11:03 +0000)]
- removed cic_cache and cic_annotations_cache
- moved metadata before tactics

20 years agoadded term_of_uri
Stefano Zacchiroli [Wed, 20 Oct 2004 10:54:33 +0000 (10:54 +0000)]
added term_of_uri

20 years agosnapshot, still work in progress
Stefano Zacchiroli [Wed, 20 Oct 2004 10:31:50 +0000 (10:31 +0000)]
snapshot, still work in progress

20 years agotop level query module
Stefano Zacchiroli [Wed, 20 Oct 2004 10:31:37 +0000 (10:31 +0000)]
top level query module

20 years agobroken
Stefano Zacchiroli [Mon, 18 Oct 2004 14:00:33 +0000 (14:00 +0000)]
broken

20 years agoremoved cicCache (cicEnvironment should be used instead)
Stefano Zacchiroli [Mon, 18 Oct 2004 13:57:52 +0000 (13:57 +0000)]
removed cicCache (cicEnvironment should be used instead)

20 years agoimplemented here at_least constraints matching engine
Stefano Zacchiroli [Mon, 18 Oct 2004 13:49:01 +0000 (13:49 +0000)]
implemented here at_least constraints matching engine

20 years agoadded helm-metadata module
Stefano Zacchiroli [Fri, 15 Oct 2004 14:12:17 +0000 (14:12 +0000)]
added helm-metadata module

20 years agoremoved some old debugging messages
Stefano Zacchiroli [Fri, 15 Oct 2004 14:09:32 +0000 (14:09 +0000)]
removed some old debugging messages

20 years agomoved string_of_uriref to UriManager
Stefano Zacchiroli [Fri, 15 Oct 2004 14:08:45 +0000 (14:08 +0000)]
moved string_of_uriref to UriManager

20 years agomoved string_of_uriref from MQueryMisc to UriManager
Stefano Zacchiroli [Fri, 15 Oct 2004 14:08:00 +0000 (14:08 +0000)]
moved string_of_uriref from MQueryMisc to UriManager

20 years agoLuca (bugged) debugging stuff removed.
Claudio Sacerdoti Coen [Thu, 14 Oct 2004 10:52:59 +0000 (10:52 +0000)]
Luca (bugged) debugging stuff removed.

20 years agofixed make dep command
Stefano Zacchiroli [Thu, 14 Oct 2004 10:12:44 +0000 (10:12 +0000)]
fixed make dep command

20 years agono_inconcl_aux managed
Claudio Sacerdoti Coen [Thu, 14 Oct 2004 09:32:53 +0000 (09:32 +0000)]
no_inconcl_aux managed

20 years ago* create_mowgli_tables.mysql.sql added
Claudio Sacerdoti Coen [Thu, 14 Oct 2004 09:32:16 +0000 (09:32 +0000)]
* create_mowgli_tables.mysql.sql added
* fill_inconcl_aux.sql added (what does it do? Ask Andrea or Selmi)

20 years agosnapshot
Stefano Zacchiroli [Wed, 13 Oct 2004 09:50:44 +0000 (09:50 +0000)]
snapshot

20 years agoadded alias for cic_textual_parser2
Stefano Zacchiroli [Wed, 13 Oct 2004 09:45:16 +0000 (09:45 +0000)]
added alias for cic_textual_parser2

20 years agosnapshot, notably history no longer remember annotations: they are
Stefano Zacchiroli [Wed, 13 Oct 2004 08:17:57 +0000 (08:17 +0000)]
snapshot, notably history no longer remember annotations: they are
computed on the fly

20 years agotransformations no longer use Content_expression, but rather CicAst
Stefano Zacchiroli [Wed, 13 Oct 2004 08:16:45 +0000 (08:16 +0000)]
transformations no longer use Content_expression, but rather CicAst

20 years agopretty printed Absurd's term
Stefano Zacchiroli [Wed, 13 Oct 2004 08:06:10 +0000 (08:06 +0000)]
pretty printed Absurd's term

20 years agoadded term argument to absurd
Stefano Zacchiroli [Wed, 13 Oct 2004 08:04:55 +0000 (08:04 +0000)]
added term argument to absurd

20 years agoget_and_save now handles big files properly (i.e. doesn't hold them
Andrea Asperti [Wed, 13 Oct 2004 07:18:40 +0000 (07:18 +0000)]
get_and_save now handles big files properly (i.e. doesn't hold them
entirely in memory)

20 years agoported to ocaml-http 0.0.10 (renamed Http_client -> Http_user_agent)
Stefano Zacchiroli [Tue, 12 Oct 2004 21:01:23 +0000 (21:01 +0000)]
ported to ocaml-http 0.0.10 (renamed Http_client -> Http_user_agent)