Since several weeks whelp did not compile any longer. Fixed:
1. the new getter implementation by Zack does not implement yet remote
calls. I have changed the (sample) configuration file to use an internal
getter (maybe also speeding up the tool?)
2. the new parser implementation does not have hard-coded notation. The
notation is now loaded from two files on disk (core_notation.moo and
coq.moo). I have added to entries in the configuration file to hold the
path to the two moo files.
3. Whelp needs to parse and pretty-print the alias definitions. The old
parser and pretty-printer was removed from CVS. I have re-used the new
pretty-printer, but no parser was available. I have reimplemented it
(in DisambiguatePp :-). The file should probably be renamed. Moreover,
the code implemented is very redundant with the corresponding one in
MatitaEngine
WARNING: this commit changes the DB representation; you need to alter the
DB by hand after this commit
- h_position: varchar(255) -> varchar(62)
- h_sort: varchar(255) -> varchar(6)
- several indexes have been redesigned from scratch.
Motivation: MySql is not able to exploit two indexes (on columns c1 and c2)
in a query of type "select ... from table where c1 = x and c2 = y".
Only one of the two indexes is exploited; the other test is done on each line. My commit introduces a single index on c1 AND c2 in place of two indexes.
WARNING: it is sure that a few queries (e.g. match) are greatly optimized by
this commit. On the contrary I ignore if the performance of other queries drops.Moreover, I have not optimized yet the indexes over the hits and count tables.
WARNING: this commit changes the DB representation; you need to alter the
DB by hand after this commit
- h_position: varchar(255) -> varchar(62)
- h_sort: varchar(255) -> varchar(6)
- several indexes have been redesigned from scratch.
Motivation: MySql is not able to exploit two indexes (on columns c1 and c2)
in a query of type "select ... from table where c1 = x and c2 = y".
Only one of the two indexes is exploited; the other test is done on each line.
My commit introduces a single index on c1 AND c2 in place of two indexes.
WARNING: it is sure that a few queries (e.g. match) are greatly optimized by
this commit. On the contrary I ignore if the performance of other queries drops.
Moreover, I have not optimized yet the indexes over the hits and count tables.
Partial bug fix: every inner type is now added to the selection roots.
However, the inner types are not closed terms! They live in the context of
their terms. Right now there is a bug in locating subterms of a proof.
Thus I do not even try to fix inner types selection properly.
0. core_notation.ma splitted into coq.moo and core_notation.moo
1. 'include "coq.ma"' is now explicitly required to activate the notation of Coq
2. 'include "coq.ma"' added here and there in the tests
3. .ma headers updated
- re-factoring: dropped sequentViewer in favour of cicMathView which
handles rendering of both sequents and objects
- added preliminary support for selection in cicBrowser
(there are still issues with phisical equality and multiple xrefs ...)
1. ProofEngineHelpers.locate_in_term, ProofEngineHelpers.locate_in_conjecture
generalized to return the list of matched terms
2. unfold generalized to unfold several occurrences at once
REVERT OF MY PREVIOUS COMMIT THAT INTRODUCES A CRITICAL BUG (some lines
are automatically _removed_ from the script). I will commit again as soon
as I fix the bug.
Management of automatic insertion of aliases and "goal" commands reimplemented
almost from scratch. The new commands inserted are now distinct entities in
the history. As a consequence going up in the script is now a step by step
operation and going up and going down are invertible operations, as they
should be.
fixed matitamake to handle development with names with spaces
the engine now has 2 different exception to report 2 diffrent problems:
- UnableToInclude
- IncluedFileNotCompiled
refactored gui handling code so that MatitaMathView is linked before MatitaGui
and all callback registrations happen in matitaGui.ml rather than matita.ml
Bug solved: the #reparent method of Gtk should NOT be used:
see http://www.gtk.org/faq/#AEN636.
This solves the flickering problem that occurred when a new tab was selected.
After the disambiguation, if the term is no longer ambiguous, we forget the
environment. In this way we are forced to do more work later (since we have
less aliases), but we have more freedom (since we have less aliases) in the
future disambiguations.
projects / helm.git / log