]> matita.cs.unibo.it Git - helm.git/log
helm.git
13 years agotrans_eq and sym_eq indexing restored. Apparently they are useful for several(?)
Claudio Sacerdoti Coen [Wed, 2 Nov 2011 12:57:20 +0000 (12:57 +0000)]
trans_eq and sym_eq indexing restored. Apparently they are useful for several(?)
theorems in CerCo (file positive.ma).

13 years agoMatitaweb: Added jquery.js (also used in some of the previous releases).
Wilmer Ricciotti [Wed, 2 Nov 2011 12:54:29 +0000 (12:54 +0000)]
Matitaweb: Added jquery.js (also used in some of the previous releases).

13 years agoMatitaweb:
Wilmer Ricciotti [Wed, 2 Nov 2011 12:52:37 +0000 (12:52 +0000)]
Matitaweb:
1) Added button to strip interpretations from the source
2) Fixed some UI bugs

13 years agoThe proof of append_cons used transitive_eq, not indexed.
Andrea Asperti [Wed, 2 Nov 2011 10:58:34 +0000 (10:58 +0000)]
The proof of append_cons used transitive_eq, not indexed.
If other cases will present we shall reindex it.

13 years agoDisabled printings.
Andrea Asperti [Wed, 2 Nov 2011 10:29:00 +0000 (10:29 +0000)]
Disabled printings.

13 years ago--Tre the expected branching with the actual one and
Andrea Asperti [Wed, 2 Nov 2011 10:23:45 +0000 (10:23 +0000)]
--Tre the expected branching with the actual one and
       prune the candidate when the latter is larger. The optimization
              is meant to rule out stange applications of flexible terms,
                     such as the application of eq_f that always succeeds.
                            There is some gain but less than expected

                            :his line, and those below, will be ignored--

M    ng_tactics/nnAuto.ml

13 years agocommit by user andrea
matitaweb [Fri, 28 Oct 2011 14:37:01 +0000 (14:37 +0000)]
commit by user andrea

13 years agoMatitaweb: added layout.js (currently manages resizing of UI).
Wilmer Ricciotti [Fri, 28 Oct 2011 13:49:57 +0000 (13:49 +0000)]
Matitaweb: added layout.js (currently manages resizing of UI).

13 years agoNew management of resulting subst in deep_eq: used to be malformed.
Andrea Asperti [Fri, 28 Oct 2011 10:59:33 +0000 (10:59 +0000)]
New management of resulting subst in deep_eq: used to be malformed.

13 years ago-applicative_case has been rewritten and simplified;
Andrea Asperti [Fri, 28 Oct 2011 10:58:22 +0000 (10:58 +0000)]
-applicative_case has been rewritten and simplified;
 the strategy should be clear, now.
- if we have an unkown ?n goal we instantiate it with I:True:Prop.
  Due to the topological ordering of goals, ?n should not appear
  in any other open goal, so its instantiation can be arbitrary.
- paramodulation is has only an implicit knowledge of the symmetry
  of equality, hence it is in trouble to prove (a=b) = (b=a).
  A try_sym tactic has been added to smart application to cover this
  case.

13 years agoSome qed-
Andrea Asperti [Fri, 28 Oct 2011 09:34:23 +0000 (09:34 +0000)]
Some qed-

13 years agosome qed-
Andrea Asperti [Fri, 28 Oct 2011 09:33:44 +0000 (09:33 +0000)]
some qed-

13 years agoNew management of the resulting substitution in deep eq.
Andrea Asperti [Fri, 28 Oct 2011 08:40:50 +0000 (08:40 +0000)]
New management of the resulting substitution in deep eq.
We reduced several time the goal vs the active table, possibly
resulting in a clash of names generating cyclic substitutions.

13 years ago-pplicative_case has been rewritten and simplified;
Andrea Asperti [Fri, 28 Oct 2011 08:13:03 +0000 (08:13 +0000)]
-pplicative_case has been rewritten and simplified;
  the strategy should be clear, now.
  - if we have an unkown ?n goal we instantiate it with I:True:Prop.
    Due to the topological ordering of goals, ?n should not appear
      in any other open goal, so its instantiation can be arbitrary.
      - paramodulation is has only an implicit knowledge of the symmetry
        of equality, hence it is in trouble to prove (a=b) = (b=a).
          A try_sym tactic has been added to smart application to cover this
            case.-This line, and those below, will be ignored--

M    nnAuto.ml

13 years agoMatitaweb: Fixed a bug in matitaweb.js concerning disambiguation and escaping.
Wilmer Ricciotti [Thu, 27 Oct 2011 11:32:11 +0000 (11:32 +0000)]
Matitaweb: Fixed a bug in matitaweb.js concerning disambiguation and escaping.
Added pretty-printing of unhandled NTacStatus.Error exceptions.

13 years agorefactoring ...
Ferruccio Guidi [Wed, 26 Oct 2011 08:31:53 +0000 (08:31 +0000)]
refactoring ...

13 years ago-- some renaming in basic_2
Ferruccio Guidi [Tue, 25 Oct 2011 12:27:34 +0000 (12:27 +0000)]
-- some renaming in basic_2

13 years agoold pr2_subst1 (Basic-1) closed!
Ferruccio Guidi [Tue, 25 Oct 2011 12:21:04 +0000 (12:21 +0000)]
old pr2_subst1 (Basic-1) closed!

13 years agoMatitaweb: first attempt at web UI for disambiguation.
Wilmer Ricciotti [Mon, 24 Oct 2011 16:40:58 +0000 (16:40 +0000)]
Matitaweb: first attempt at web UI for disambiguation.
Also includes a rather radical change in the way the graphical layout is
handled.

13 years agoNow it should compile :-)
Andrea Asperti [Fri, 21 Oct 2011 15:35:14 +0000 (15:35 +0000)]
Now it should compile :-)

13 years agoOptimization. Check removed.
Andrea Asperti [Fri, 21 Oct 2011 07:26:43 +0000 (07:26 +0000)]
Optimization. Check removed.

13 years agoDisabled debug.
Andrea Asperti [Fri, 21 Oct 2011 06:49:56 +0000 (06:49 +0000)]
Disabled debug.

13 years ago1. ported to camlp5
Andrea Asperti [Thu, 20 Oct 2011 16:16:24 +0000 (16:16 +0000)]
1. ported to camlp5
2. added a boolean to qed to governe indexing
   the syntax for disabling indexing is "qed-"

13 years agotypos
Andrea Asperti [Thu, 20 Oct 2011 16:13:06 +0000 (16:13 +0000)]
typos

13 years agoWe order alternatives according to the number of subgoals they open.
Andrea Asperti [Thu, 20 Oct 2011 15:54:22 +0000 (15:54 +0000)]
We order alternatives according to the number of subgoals they open.

13 years agoQED takes a boolean parameter governing indexing.
Andrea Asperti [Thu, 20 Oct 2011 15:49:59 +0000 (15:49 +0000)]
QED takes a boolean parameter governing indexing.
Syntax to avoid indexing is qed-

13 years agoAlternatives are ordered according to the number of subgoals
Andrea Asperti [Thu, 20 Oct 2011 15:47:59 +0000 (15:47 +0000)]
Alternatives are ordered according to the number of subgoals
they generate.

13 years agoJMeq lifted to work on Type[1].
Wilmer Ricciotti [Thu, 20 Oct 2011 13:58:55 +0000 (13:58 +0000)]
JMeq lifted to work on Type[1].

13 years agoRemoved some unneeded normalizations from the generation of discrimination
Wilmer Ricciotti [Thu, 20 Oct 2011 12:49:31 +0000 (12:49 +0000)]
Removed some unneeded normalizations from the generation of discrimination
principles (they had a bad effect on performance).

13 years agoMatitaweb: added preliminary support for interactive disambiguation.
Wilmer Ricciotti [Thu, 20 Oct 2011 10:45:34 +0000 (10:45 +0000)]
Matitaweb: added preliminary support for interactive disambiguation.
Ambiguous expressions are reported to the client and highlighted.
The possible interpretations are shown in stderr.

13 years agoMatitaweb: added a function MatitaAuthentication.get_users returning
matitaweb [Wed, 19 Oct 2011 15:58:38 +0000 (15:58 +0000)]
Matitaweb: added a function MatitaAuthentication.get_users returning
the list of the registered users.

13 years ago- the relocation properties of cpr are closed!
Ferruccio Guidi [Wed, 19 Oct 2011 15:57:18 +0000 (15:57 +0000)]
- the relocation properties of cpr are closed!
- the support for global references is started ...
- some refactoring.

13 years agocommit by user andrea
matitaweb [Wed, 19 Oct 2011 10:34:46 +0000 (10:34 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Wed, 19 Oct 2011 08:07:45 +0000 (08:07 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Wed, 19 Oct 2011 07:09:27 +0000 (07:09 +0000)]
commit by user andrea

13 years agoLocalization of errors.
matitaweb [Tue, 18 Oct 2011 15:41:04 +0000 (15:41 +0000)]
Localization of errors.

13 years agoChanges in "destruct" tactic (allowing performance improvements):
Wilmer Ricciotti [Tue, 18 Oct 2011 09:40:12 +0000 (09:40 +0000)]
Changes in "destruct" tactic (allowing performance improvements):
1) discrimination principles are now generated upon definition of an inductive
   type I and recorded as objects I_discr and I_jmdiscr (resp. leibniz and john
   major's principles); in case JMeq wasn't loaded at that time, it is possible
   to explicitly request the definition by means of the command

   discriminator I.

2) destruct uses the aforementioned principle rather than generating a cut at
   each discrimination step

3) destruct performs generalizations using the basic generalize0_tac, rather
   than generalize_tac: this should bring small performance improvements.

13 years agocompact coercion command: "coercion foo."
Enrico Tassi [Mon, 17 Oct 2011 13:24:47 +0000 (13:24 +0000)]
compact coercion command: "coercion foo."

13 years agocommit by user andrea
matitaweb [Mon, 17 Oct 2011 13:02:43 +0000 (13:02 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Mon, 17 Oct 2011 10:51:01 +0000 (10:51 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Mon, 17 Oct 2011 09:12:35 +0000 (09:12 +0000)]
commit by user andrea

13 years agocommit by user lroversi
matitaweb [Mon, 17 Oct 2011 07:13:18 +0000 (07:13 +0000)]
commit by user lroversi

13 years agocommit by user andrea
matitaweb [Fri, 14 Oct 2011 14:31:37 +0000 (14:31 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Fri, 14 Oct 2011 11:20:38 +0000 (11:20 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Fri, 14 Oct 2011 10:45:24 +0000 (10:45 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Fri, 14 Oct 2011 10:44:57 +0000 (10:44 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Fri, 14 Oct 2011 10:33:03 +0000 (10:33 +0000)]
commit by user andrea

13 years agoMade a copy of basics/list.ma as a base for chapter 3.
matitaweb [Fri, 14 Oct 2011 09:07:07 +0000 (09:07 +0000)]
Made a copy of basics/list.ma as a base for chapter 3.

13 years agocommit by user andrea
matitaweb [Fri, 14 Oct 2011 08:05:26 +0000 (08:05 +0000)]
commit by user andrea

13 years agocommit by user enrico
matitaweb [Thu, 13 Oct 2011 21:09:09 +0000 (21:09 +0000)]
commit by user enrico

13 years agocommit by user andrea
matitaweb [Thu, 13 Oct 2011 15:46:31 +0000 (15:46 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Thu, 13 Oct 2011 15:38:26 +0000 (15:38 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Thu, 13 Oct 2011 15:31:43 +0000 (15:31 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Thu, 13 Oct 2011 15:25:40 +0000 (15:25 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Wed, 12 Oct 2011 15:49:17 +0000 (15:49 +0000)]
commit by user andrea

13 years agoMatitaweb: Fixed netplex.conf (which was changed by mistake in the previous commit).
Wilmer Ricciotti [Wed, 12 Oct 2011 14:13:27 +0000 (14:13 +0000)]
Matitaweb: Fixed netplex.conf (which was changed by mistake in the previous commit).

13 years agoMatitaweb: svn now skips empty commits.
Wilmer Ricciotti [Wed, 12 Oct 2011 14:02:22 +0000 (14:02 +0000)]
Matitaweb: svn now skips empty commits.

13 years agocommit by user andrea
matitaweb [Wed, 12 Oct 2011 14:00:06 +0000 (14:00 +0000)]
commit by user andrea

13 years agoMatitaweb: svn now skips empty add.
Wilmer Ricciotti [Wed, 12 Oct 2011 13:59:15 +0000 (13:59 +0000)]
Matitaweb: svn now skips empty add.

13 years agocommit by user lroversi
matitaweb [Wed, 12 Oct 2011 13:52:23 +0000 (13:52 +0000)]
commit by user lroversi

13 years agoAdministrative commit restoring the repository to the usual shape.
matitaweb [Wed, 12 Oct 2011 13:05:01 +0000 (13:05 +0000)]
Administrative commit restoring the repository to the usual shape.

13 years agocommit by user ricciott
matitaweb [Wed, 12 Oct 2011 12:55:15 +0000 (12:55 +0000)]
commit by user ricciott

13 years agotheory of ltpss completed!
Ferruccio Guidi [Wed, 12 Oct 2011 12:01:06 +0000 (12:01 +0000)]
theory of ltpss completed!

13 years agocommit by user andrea
matitaweb [Wed, 12 Oct 2011 11:41:37 +0000 (11:41 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Wed, 12 Oct 2011 11:06:00 +0000 (11:06 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Wed, 12 Oct 2011 07:45:41 +0000 (07:45 +0000)]
commit by user andrea

13 years agoupdate ...
Ferruccio Guidi [Tue, 11 Oct 2011 17:43:01 +0000 (17:43 +0000)]
update ...

13 years agoupdate ...
Ferruccio Guidi [Tue, 11 Oct 2011 17:34:12 +0000 (17:34 +0000)]
update ...

13 years ago- cpr_lsubs_conf proved! (was pr2_change)
Ferruccio Guidi [Tue, 11 Oct 2011 17:27:11 +0000 (17:27 +0000)]
- cpr_lsubs_conf proved! (was pr2_change)
- some "-" removed :)

13 years agocommit by user andrea
matitaweb [Tue, 11 Oct 2011 16:26:12 +0000 (16:26 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Tue, 11 Oct 2011 16:24:14 +0000 (16:24 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Tue, 11 Oct 2011 15:48:50 +0000 (15:48 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Tue, 11 Oct 2011 15:39:38 +0000 (15:39 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Tue, 11 Oct 2011 14:35:51 +0000 (14:35 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Tue, 11 Oct 2011 14:18:38 +0000 (14:18 +0000)]
commit by user andrea

13 years agorefactoring completed!
Ferruccio Guidi [Tue, 11 Oct 2011 12:37:58 +0000 (12:37 +0000)]
refactoring completed!

13 years agoMatitaweb: Fixed long-time bug with dependencies and makefiles.
Wilmer Ricciotti [Tue, 11 Oct 2011 12:31:11 +0000 (12:31 +0000)]
Matitaweb: Fixed long-time bug with dependencies and makefiles.

13 years agoChapter 2
matitaweb [Tue, 11 Oct 2011 11:47:55 +0000 (11:47 +0000)]
Chapter 2

13 years agocommit by user utente1
matitaweb [Tue, 11 Oct 2011 11:09:25 +0000 (11:09 +0000)]
commit by user utente1

13 years agocommit by user andrea
matitaweb [Tue, 11 Oct 2011 11:08:50 +0000 (11:08 +0000)]
commit by user andrea

13 years agoWARNING: major experimental change.
Claudio Sacerdoti Coen [Tue, 11 Oct 2011 10:43:54 +0000 (10:43 +0000)]
WARNING: major experimental change.

"include" is no longer turned into an "include alias"
when the file to be included is already loaded. This
greatly speeds up inclusion, at the price of having
to manually add some "include alias" here and there.

13 years agoNew version (by Wilmer). The main difference w.r.t. previous one
Claudio Sacerdoti Coen [Tue, 11 Oct 2011 00:26:29 +0000 (00:26 +0000)]
New version (by Wilmer). The main difference w.r.t. previous one
is that it should not normalize the hypotheses and the conclusion
without any need to do that.

BEWARE: this version seems to be a little buggy. See "Wilmer: XXX"
comments in CerCo files. I commit it anyway and let the debug to
Wilmer. It only fails in three places.

13 years agorefactoring ...
Ferruccio Guidi [Mon, 10 Oct 2011 18:36:03 +0000 (18:36 +0000)]
refactoring ...

13 years agorefactoring ...
Ferruccio Guidi [Mon, 10 Oct 2011 17:39:08 +0000 (17:39 +0000)]
refactoring ...

13 years agocpr_cast closed! (after a bugfix in the "destruct" tactic)
Ferruccio Guidi [Mon, 10 Oct 2011 17:17:33 +0000 (17:17 +0000)]
cpr_cast closed! (after a bugfix in the "destruct" tactic)

13 years ago1. nInversion/nDestruct ported to work with jmeq properly
Claudio Sacerdoti Coen [Mon, 10 Oct 2011 13:52:59 +0000 (13:52 +0000)]
1. nInversion/nDestruct ported to work with jmeq properly
2. axiom streicherK in logic.ma replaced with a computational proof
3. library changed accordingly

13 years agoDebugging code commented out.
Claudio Sacerdoti Coen [Mon, 10 Oct 2011 12:34:52 +0000 (12:34 +0000)]
Debugging code commented out.

13 years agoPorted changes amde on the main branch:
Andrea Asperti [Mon, 10 Oct 2011 12:18:57 +0000 (12:18 +0000)]
Ported changes amde on the main branch:
1. Reintroduced a failure cache
2. Corrected a bug in subsumption
3. Crippled the search space of not-last (side) equational goals.

13 years ago- Reintroduction of a failure chache
Andrea Asperti [Mon, 10 Oct 2011 11:23:53 +0000 (11:23 +0000)]
- Reintroduction of a failure chache
-r
-e, and those below, will be ignored--

    ng_tactics/nnAuto.ml

13 years agoMatitaweb: fixed bugs in commit.
matitaweb [Fri, 7 Oct 2011 13:05:04 +0000 (13:05 +0000)]
Matitaweb: fixed bugs in commit.

13 years agocommit by user utente3
matitaweb [Fri, 7 Oct 2011 13:03:52 +0000 (13:03 +0000)]
commit by user utente3

13 years agocommit by user utente2
matitaweb [Fri, 7 Oct 2011 12:20:08 +0000 (12:20 +0000)]
commit by user utente2

13 years agoMatitaweb: added a titlebar to the GUI.
Wilmer Ricciotti [Thu, 6 Oct 2011 15:19:26 +0000 (15:19 +0000)]
Matitaweb: added a titlebar to the GUI.

13 years agoMatitaweb: more changes to commit (now almost usable).
Wilmer Ricciotti [Thu, 6 Oct 2011 12:20:27 +0000 (12:20 +0000)]
Matitaweb: more changes to commit (now almost usable).

13 years agocommit by user utente
Wilmer Ricciotti [Wed, 5 Oct 2011 12:23:45 +0000 (12:23 +0000)]
commit by user utente

13 years agoMatitaweb: several improvements to svn interface.
matitaweb [Wed, 5 Oct 2011 10:44:08 +0000 (10:44 +0000)]
Matitaweb: several improvements to svn interface.
Some cosmetic changes.

13 years agonews update
Ferruccio Guidi [Mon, 3 Oct 2011 18:37:18 +0000 (18:37 +0000)]
news update

13 years agotypos ...
Ferruccio Guidi [Mon, 3 Oct 2011 18:15:41 +0000 (18:15 +0000)]
typos ...

13 years ago- first version of xhtbl
Ferruccio Guidi [Mon, 3 Oct 2011 17:59:46 +0000 (17:59 +0000)]
- first version of xhtbl
- first version of ld_basic_2.html (generated)

13 years ago- new stylesheets for xhtml pages (ld_web)
Ferruccio Guidi [Mon, 3 Oct 2011 15:26:05 +0000 (15:26 +0000)]
- new stylesheets for xhtml pages (ld_web)
- typo corrected in ld_web.css