]> matita.cs.unibo.it Git - helm.git/log
projects / helm.git / log
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
helm.git
19 years agoadded script support
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 18 Jan 2005 18:17:33 +0000 (18:17 +0000)]
added script support

19 years agoadded latex style comment, with start token "%%"
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 18 Jan 2005 18:16:43 +0000 (18:16 +0000)]
added latex style comment, with start token "%%"

19 years agoremoved spurious debugging prints
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 18 Jan 2005 18:15:57 +0000 (18:15 +0000)]
removed spurious debugging prints

19 years agosnapshot, notably:
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 18 Jan 2005 18:15:25 +0000 (18:15 +0000)]
snapshot, notably:
- first commit of matitac

19 years agofixed comments
commit | commitdiff | tree
Enrico Tassi [Tue, 18 Jan 2005 09:21:25 +0000 (09:21 +0000)]
fixed comments

19 years ago- added helm_ns and xhtml_ns (XHTML and HELM namespace, respectively)
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 17 Jan 2005 16:24:22 +0000 (16:24 +0000)]
- added helm_ns and xhtml_ns (XHTML and HELM namespace, respectively)
- changed usage string so that it is a well fermod XHTML document (added
  namespace, quoted ampersands)

19 years agonew cicEnvironment implementation
commit | commitdiff | tree
Enrico Tassi [Mon, 17 Jan 2005 16:24:17 +0000 (16:24 +0000)]
new cicEnvironment implementation

19 years agoNo longer return HTTP 400 answers or non-xml answers: all document returned
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 17 Jan 2005 16:23:26 +0000 (16:23 +0000)]
No longer return HTTP 400 answers or non-xml answers: all document returned
by the getter are now XHTML documents, possibly with the addition of an
attribute helm:exception on the root <html> element in the
http://www.cs.unibo.it/helm namespace. The presence of such an attribute
means that an exception has occured, its value is meant to be a string
encoding of the relevant ocaml exception

19 years agofirst (almost) working version: apparently, only generation of coinductive
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 17 Jan 2005 14:53:03 +0000 (14:53 +0000)]
first (almost) working version: apparently, only generation of coinductive
eliminators does not typecheck

19 years agosnapshot, notably:
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 14 Jan 2005 17:35:26 +0000 (17:35 +0000)]
snapshot, notably:
- changed interface, now returns a Cic.obj
- added consistency check between generated body and type

19 years agosnapshot (1st commit of fix body generation)
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 13 Jan 2005 07:08:55 +0000 (07:08 +0000)]
snapshot (1st commit of fix body generation)

19 years agofixed clean_and_fill
commit | commitdiff | tree
Enrico Tassi [Wed, 12 Jan 2005 15:08:35 +0000 (15:08 +0000)]
fixed clean_and_fill

19 years agofixed bug in fill_and_clean (now the helper universes_of_obj knows that
commit | commitdiff | tree
Enrico Tassi [Wed, 12 Jan 2005 14:56:46 +0000 (14:56 +0000)]
fixed bug in fill_and_clean (now the helper universes_of_obj knows that
the uri passed as the first parameter can't be in the environment and it
doesn't requests it)

19 years agosnapshot, notably:
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 16:11:12 +0000 (16:11 +0000)]
snapshot, notably:
- added support for inductive definitions
- prelimnary support for user searches

19 years agoadded fallback case (assertion failure) for unsupported Implicit annotations
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 16:09:20 +0000 (16:09 +0000)]
added fallback case (assertion failure) for unsupported Implicit annotations

19 years agoadded syntax for URIs
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 16:08:24 +0000 (16:08 +0000)]
added syntax for URIs

19 years agoadded search commands
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 16:05:23 +0000 (16:05 +0000)]
added search commands

19 years ago- added pack/unpack over AST of terms
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 16:04:31 +0000 (16:04 +0000)]
- added pack/unpack over AST of terms
- created cicAst.mli (it was missing)

19 years ago- added pack/unpack over AST of terms
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 16:04:31 +0000 (16:04 +0000)]
- added pack/unpack over AST of terms
- created cicAst.mli (it was missing)
- added syntax for URIs

19 years agoadded clean_and_fill, to be invoked on qed
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 16:03:13 +0000 (16:03 +0000)]
added clean_and_fill, to be invoked on qed

19 years agosnapshot, not yet completed, but ...
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 16:02:53 +0000 (16:02 +0000)]
snapshot, not yet completed, but ...

19 years ago- added support for contexts (terms with holes)
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 16:01:46 +0000 (16:01 +0000)]
- added support for contexts (terms with holes)
- added CicUtil.pack/unpack to pack/unpack several terms in a single term
- added CicUtil.strip_prods to removed a given number of head prods from a term
- added CicUtil.context_of/select to create contexts/select a subterm
  matching a context

19 years agocosmetic changes
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 15:59:06 +0000 (15:59 +0000)]
cosmetic changes

19 years agoadded begin list and end list comments to help moogle search engine plugin
commit | commitdiff | tree
Enrico Tassi [Mon, 10 Jan 2005 10:47:47 +0000 (10:47 +0000)]
added begin list and end list comments to help moogle search engine plugin

19 years agoexported lift_from
commit | commitdiff | tree
Stefano Zacchiroli [Wed, 5 Jan 2005 14:07:33 +0000 (14:07 +0000)]
exported lift_from

19 years agosnapshot
commit | commitdiff | tree
Stefano Zacchiroli [Wed, 5 Jan 2005 14:06:41 +0000 (14:06 +0000)]
snapshot

19 years agoadded an hyperlink to the input syntax page
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 21 Dec 2004 17:52:32 +0000 (17:52 +0000)]
added an hyperlink to the input syntax page

19 years agoimproved input syntax page with example queries of elim, match and hint
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 21 Dec 2004 17:48:59 +0000 (17:48 +0000)]
improved input syntax page with example queries of elim, match and hint

19 years agoadded URI printing in the result page (so that mouse-over is not the
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 21 Dec 2004 17:19:40 +0000 (17:19 +0000)]
added URI printing in the result page (so that mouse-over is not the
only way to know the URI of results!)

19 years agofirst commit (in the wrong place --by CSC) of induction principles generation
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 21 Dec 2004 15:49:03 +0000 (15:49 +0000)]
first commit (in the wrong place --by CSC) of induction principles generation

19 years agoignores example binaries
commit | commitdiff | tree
Stefano Zacchiroli [Sat, 11 Dec 2004 16:32:14 +0000 (16:32 +0000)]
ignores example binaries

19 years agoported to new format of Parse_error exception (which includes error position)
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 9 Dec 2004 20:31:24 +0000 (20:31 +0000)]
ported to new format of Parse_error exception (which includes error position)

19 years ago(dummy) porting to universes
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 9 Dec 2004 20:29:44 +0000 (20:29 +0000)]
(dummy) porting to universes

19 years agoimplemented pretty printer for (mutual) (co)inductive types
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 9 Dec 2004 17:20:56 +0000 (17:20 +0000)]
implemented pretty printer for (mutual) (co)inductive types

19 years ago(first) complete implementation of (mutual) (co)inductive types syntax
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 9 Dec 2004 17:20:06 +0000 (17:20 +0000)]
(first) complete implementation of (mutual) (co)inductive types syntax

19 years agoaddded inductive definition to AST
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 9 Dec 2004 15:18:50 +0000 (15:18 +0000)]
addded inductive definition to AST

19 years ago- enriched Parse_error exception with error location
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 9 Dec 2004 15:18:30 +0000 (15:18 +0000)]
- enriched Parse_error exception with error location
- first implementation of inductive type definitions (not yet completed:
  mutual inductive definition are still missing)
- test parser now displays error location using ASCII escape coloring

19 years agosymmetry of equality NOT used in auto
commit | commitdiff | tree
Andrea Asperti [Tue, 7 Dec 2004 08:25:12 +0000 (08:25 +0000)]
symmetry of equality NOT used in auto

19 years agoNew version of auto with "width".
commit | commitdiff | tree
Andrea Asperti [Mon, 6 Dec 2004 12:16:07 +0000 (12:16 +0000)]
New version of auto with "width".

19 years agosnapshot
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 3 Dec 2004 16:30:13 +0000 (16:30 +0000)]
snapshot

19 years agomoogle syntax help page, actually contains only syntax and examples for
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 3 Dec 2004 16:05:27 +0000 (16:05 +0000)]
moogle syntax help page, actually contains only syntax and examples for
the "locate" query. "hint", "match" and "elim" syntaxes are currently
undocumented

19 years agochanged "locate" so that it supports shell-like pattern matching with
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 3 Dec 2004 16:04:01 +0000 (16:04 +0000)]
changed "locate" so that it supports shell-like pattern matching with
'*' and '?' wildcards

19 years agoported to universes
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 3 Dec 2004 15:13:29 +0000 (15:13 +0000)]
ported to universes

19 years ago*** empty log message ***
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 2 Dec 2004 14:55:54 +0000 (14:55 +0000)]
*** empty log message ***

19 years agosync with universes and ~subst (and not ?(subst=[]))
commit | commitdiff | tree
Enrico Tassi [Thu, 2 Dec 2004 13:43:58 +0000 (13:43 +0000)]
sync with universes and ~subst (and not ?(subst=[]))

19 years agoAdded universes handling. Tag PRE_UNIVERSES may help ;)
commit | commitdiff | tree
Enrico Tassi [Wed, 1 Dec 2004 09:43:44 +0000 (09:43 +0000)]
Added universes handling. Tag PRE_UNIVERSES may help ;)

19 years agoAdded universes handling. The PRE_UNIVERSES tag may help ;)
commit | commitdiff | tree
Enrico Tassi [Wed, 1 Dec 2004 09:42:42 +0000 (09:42 +0000)]
Added universes handling. The PRE_UNIVERSES tag may help ;)

19 years agoBug in the management of substitutions into auto corrected.
commit | commitdiff | tree
Andrea Asperti [Tue, 30 Nov 2004 14:55:27 +0000 (14:55 +0000)]
Bug in the management of substitutions into auto corrected.
No significative loss in performance.
Comments commented.

19 years ago- ported tests to newer PP / substitutions
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 29 Nov 2004 12:31:21 +0000 (12:31 +0000)]
- ported tests to newer PP / substitutions

19 years ago- passes subst to FreshNameGenerator
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 29 Nov 2004 12:30:31 +0000 (12:30 +0000)]
- passes subst to FreshNameGenerator
- removed some old debugging prints

19 years agoremoved old debugging prints
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 29 Nov 2004 12:30:09 +0000 (12:30 +0000)]
removed old debugging prints

19 years agopasses ~subst to FreshNameGenerator
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 29 Nov 2004 12:24:47 +0000 (12:24 +0000)]
passes ~subst to FreshNameGenerator

19 years agopasses subst to FreshNameGenerator
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 29 Nov 2004 12:24:25 +0000 (12:24 +0000)]
passes subst to FreshNameGenerator

19 years ago- pass subst to FreshNameGenerator on mk_fresh_name invocations
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 29 Nov 2004 12:24:09 +0000 (12:24 +0000)]
- pass subst to FreshNameGenerator on mk_fresh_name invocations
- removed assert failures on get_cooked_obj (rolled back last commit)
- reindented (the huuuuuuuge) eat_prods function

19 years agobugfix: FreshNameGenerator uses the type checker on mk_fresh_name
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 29 Nov 2004 12:22:23 +0000 (12:22 +0000)]
bugfix: FreshNameGenerator uses the type checker on mk_fresh_name
invocation, thus it should receive in input a subst to be passed to the
type checker in order to avoid "unknown" Metas in the term to be type
checked

19 years agobugfix in type_of_aux' which erroneously discard given substitution
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 29 Nov 2004 12:20:06 +0000 (12:20 +0000)]
bugfix in type_of_aux' which erroneously discard given substitution
(fixes a lot of CicUtil.Meta_not_found spurious exceptions)

20 years agoported to Mysql
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 26 Nov 2004 14:17:15 +0000 (14:17 +0000)]
ported to Mysql

20 years agoported to new xpointer syntax
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 26 Nov 2004 14:17:01 +0000 (14:17 +0000)]
ported to new xpointer syntax

20 years agoprotected invocations to get_cooked_obj with assertion failures
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 25 Nov 2004 09:05:18 +0000 (09:05 +0000)]
protected invocations to get_cooked_obj with assertion failures

20 years agoprotected invocations of get_cooked_obj with assertion failures
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 25 Nov 2004 09:00:35 +0000 (09:00 +0000)]
protected invocations of get_cooked_obj with assertion failures

20 years agoguard get_cooked_obj calls with assert false in case of Not_found
commit | commitdiff | tree
Stefano Zacchiroli [Wed, 24 Nov 2004 13:18:03 +0000 (13:18 +0000)]
guard get_cooked_obj calls with assert false in case of Not_found

20 years agouse get_obj instead of get_cooked_obj in order to retrieve params for
commit | commitdiff | tree
Stefano Zacchiroli [Wed, 24 Nov 2004 13:17:39 +0000 (13:17 +0000)]
use get_obj instead of get_cooked_obj in order to retrieve params for
unchecked objects (fixes "not found" bug when trust in the environment
is false)

20 years ago* several adjustments after introduction of the depth column
commit | commitdiff | tree
Luca Padovani [Tue, 23 Nov 2004 15:15:41 +0000 (15:15 +0000)]
* several adjustments after introduction of the depth column

20 years ago* validation scripts
commit | commitdiff | tree
Luca Padovani [Tue, 23 Nov 2004 13:39:24 +0000 (13:39 +0000)]
* validation scripts

20 years ago* basic infrastructure for collecting statistics
commit | commitdiff | tree
Luca Padovani [Tue, 23 Nov 2004 13:38:52 +0000 (13:38 +0000)]
* basic infrastructure for collecting statistics

20 years agoadded parse test for
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 22 Nov 2004 17:20:15 +0000 (17:20 +0000)]
added parse test for
- expat
- libxml2 (xmlreader API)
- libxml2 (SAX2 API)

20 years agoset environment trust to false to avoid dummy proof checking
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 18 Nov 2004 16:50:34 +0000 (16:50 +0000)]
set environment trust to false to avoid dummy proof checking

20 years agouse stateful logger so that the ProofChecker daemon is able to properly
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 18 Nov 2004 16:47:28 +0000 (16:47 +0000)]
use stateful logger so that the ProofChecker daemon is able to properly
indent proof checking messages

20 years agoadded a stateful logger which remember indentation level of recursive
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 18 Nov 2004 16:46:23 +0000 (16:46 +0000)]
added a stateful logger which remember indentation level of recursive
type checking

20 years agoadded set_trust to externally set the trust function (used by the proof
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 18 Nov 2004 16:45:43 +0000 (16:45 +0000)]
added set_trust to externally set the trust function (used by the proof
checking daemon)

20 years agoported to Mysql native connection
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 18 Nov 2004 13:45:18 +0000 (13:45 +0000)]
ported to Mysql native connection

20 years agoResolved problem occured when "=" in MainConclusion
commit | commitdiff | tree
Matteo Selmi [Wed, 17 Nov 2004 14:47:13 +0000 (14:47 +0000)]
Resolved problem occured when "=" in MainConclusion

20 years agoRemoved duplicated uri in sigmatch
commit | commitdiff | tree
Matteo Selmi [Wed, 17 Nov 2004 12:48:55 +0000 (12:48 +0000)]
Removed duplicated uri in sigmatch

20 years agoBug fix
commit | commitdiff | tree
Matteo Selmi [Wed, 17 Nov 2004 11:13:46 +0000 (11:13 +0000)]
Bug fix

20 years agochanged reduction tactics ast
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 15 Nov 2004 09:04:40 +0000 (09:04 +0000)]
changed reduction tactics ast

20 years agosnapshot
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 15 Nov 2004 09:03:45 +0000 (09:03 +0000)]
snapshot

20 years agoFixed an hidden occur check problem: when a Meta is being delifted,
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 12 Nov 2004 18:13:17 +0000 (18:13 +0000)]
Fixed an hidden occur check problem: when a Meta is being delifted,
apply substitution on the fly and delift the result. Previously we did
not recursively check the instantiation of the Meta.

20 years agoadded dummy entry in CicAst: UserInput
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 11 Nov 2004 13:30:45 +0000 (13:30 +0000)]
added dummy entry in CicAst: UserInput

20 years agosnapshot:
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 11 Nov 2004 13:30:11 +0000 (13:30 +0000)]
snapshot:
- changed interaction model

20 years agobumped changelog line to match upload date
commit | commitdiff | tree
Stefano Zacchiroli [Wed, 10 Nov 2004 13:22:34 +0000 (13:22 +0000)]
bumped changelog line to match upload date

20 years agodisabled debugging info
commit | commitdiff | tree
Stefano Zacchiroli [Wed, 10 Nov 2004 12:02:27 +0000 (12:02 +0000)]
disabled debugging info

20 years agoparse Baseuri command
commit | commitdiff | tree
Stefano Zacchiroli [Wed, 10 Nov 2004 12:02:21 +0000 (12:02 +0000)]
parse Baseuri command

20 years agoadded Baseuri command
commit | commitdiff | tree
Stefano Zacchiroli [Wed, 10 Nov 2004 12:01:52 +0000 (12:01 +0000)]
added Baseuri command

20 years agocommented out some timing messages
commit | commitdiff | tree
Stefano Zacchiroli [Wed, 10 Nov 2004 12:01:39 +0000 (12:01 +0000)]
commented out some timing messages

20 years agosnapshot, notably:
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 9 Nov 2004 17:23:18 +0000 (17:23 +0000)]
snapshot, notably:
- fixed "noshow" bugs in sequents notebook and proof window
- implemented interpretation choice

20 years ago* compressed statistics committed
commit | commitdiff | tree
Luca Padovani [Tue, 9 Nov 2004 15:30:33 +0000 (15:30 +0000)]
* compressed statistics committed

20 years ago- split compound fields
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 9 Nov 2004 14:38:20 +0000 (14:38 +0000)]
- split compound fields
- rounded to integer floating point values

20 years ago* snapshot
commit | commitdiff | tree
Luca Padovani [Tue, 9 Nov 2004 13:56:59 +0000 (13:56 +0000)]
* snapshot

20 years agoAggiunta l'introduzione alla prima sezione:.
commit | commitdiff | tree
Andrea Asperti [Tue, 9 Nov 2004 12:16:24 +0000 (12:16 +0000)]
Aggiunta l'introduzione alla prima sezione:.

20 years ago* output of XML file size
commit | commitdiff | tree
Luca Padovani [Tue, 9 Nov 2004 12:07:55 +0000 (12:07 +0000)]
* output of XML file size

20 years ago* fix bug detect blank nodes
commit | commitdiff | tree
Luca Padovani [Tue, 9 Nov 2004 12:05:09 +0000 (12:05 +0000)]
* fix bug detect blank nodes
* output of file size

20 years ago* added stylesheet to render the results
commit | commitdiff | tree
Luca Padovani [Tue, 9 Nov 2004 08:22:37 +0000 (08:22 +0000)]
* added stylesheet to render the results

20 years agoadded filling of no_concl_hyp
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 9 Nov 2004 08:15:43 +0000 (08:15 +0000)]
added filling of no_concl_hyp

20 years agoadded query to fill no_concl_hyp table
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 9 Nov 2004 08:14:31 +0000 (08:14 +0000)]
added query to fill no_concl_hyp table

20 years agoformatted
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 9 Nov 2004 08:14:20 +0000 (08:14 +0000)]
formatted

20 years ago* depths now in hash table
commit | commitdiff | tree
Luca Padovani [Tue, 9 Nov 2004 07:55:31 +0000 (07:55 +0000)]
* depths now in hash table

20 years ago* snapshot
commit | commitdiff | tree
Luca Padovani [Tue, 9 Nov 2004 07:37:38 +0000 (07:37 +0000)]
* snapshot

20 years ago* added a few calculations
commit | commitdiff | tree
Luca Padovani [Mon, 8 Nov 2004 22:07:09 +0000 (22:07 +0000)]
* added a few calculations

20 years ago* added .cc program (and equivalent .xsl stylesheet) for collecting
commit | commitdiff | tree
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).
commit | commitdiff | tree
Andrea Asperti [Mon, 8 Nov 2004 12:27:44 +0000 (12:27 +0000)]
First draft (introduction).

next
Unnamed repository; edit this file 'description' to name the repository.