milestone in ground_2

ground_2: added missing file
basic_2: commit of grammar completed

ground_2 milestone: multiple relocation with lists of booleans
basic_2: simplified formalization starts: partial commit of the grammar component

first constructions with classes

optional parameters added to the syntax of definitions,
like the one for Record and Inductive.

limits: we set up a different foundation
lambdadelta: Makefile updated for new version of probe

old files (re)moved

minor site update

refactoring meta files for procedural reconstruction of \lambda\delta version 1

- simplified Makefile.defs using the ?= assignment
- now the variable OCAMLPATH is available and is correctly set

scripts for lambdadelta_1 updated with minor corrections

- the `Implied attribute is now printed
  [also the `Generated attribute is printed. is this ok?]

flavour and source information exported for the objects of lambdadelta version 1

last comment was incomplete by mistake.

- Rationale
  The `Implied attribute will mark the eliminators generated by Coq
  7.3.1 added to the contrib of lambdadelta version 1.
  [the latest version of matita generates different eliminators to
   Prop (with dependences) so we cannot reuse them]
  However, these eliminators, even if provided, must not be taken into
  account when calculating the intrinsinc complexity of the contribution
  on the matita side (by the "probe" tool), because they are not taken into
  account on the Coq side, being `Generated by Coq.

  Note that the intrinsinc complexity we are interested in is the one
  accounting just for the user-defined objects in both contributions.

- probe: updated to handle the `Implied attribute

- .depend: updated

- New attribute `Implied put beside `Generated and `Provided.
  It denotes an object provided not as defined by the user, but as generated by another ITP
  New optional keyword "implied" recognized in front of:
  theorem, definition, ..., let rec, let corec
  specifies to construct an object with this new attribute.
  [still not admitted in front of inductive, coinductive, record]

typo corrected in bibliography

last commit completed :)

updated bibliography

new version of J3a submitted to JFR

- subtraction (and related notions) removed
- more lemmas

compile-time feature PROFV to profile validation without sort inclusion

grundlagen for coq with timing information

= test2 for byte and opt
- version string management updated

- multi-file exportation for teyjus
- more profiling for helena and coq

more flexibility in the exported data for Teyjus

- conditional compilation continues ...
- current run times for helena and managers in profile.txt

initial support for bytecode compilation

- simpler attribute system
- some renaming

we are optimizing the code by conditional compilation.
three tags introduced so far: EXPAND, PREPROCESS, MANAGER

new semantics of the -g option completed

- bug fix in the static analyzer allows better Pi/forall separation (exportation to grafite)
- new option -y allows to use infinity-abstraction in contexts
- ages removed from global references (the RTM computes them)
- new semantics of the -g option (w.i.p.) for a comparison with Coq

advances on exportation to prolog

command line options rearranged

new options activated
- tracing can be restricted to specific constants with -b and -e
- restricted applications are now used by default for Automath inputs
  use -n to activate extended applications
  (this may lead to longer computations)

new syntax of abstractions propagated to complete_rg

- siimplifified RTM (one register less) now counts x-steps.
  We follow our Prolog implementation more closely.

- Two bugs detected. One solved, the other does not affect the
  Grundlagen.

exportation to \lambda\delta representation in elpi

some changes in lambdadelta butterflies

- revision of ground_2 and basic_2
  lift and drop now accept infinity as first parameter
- Makefile: updated for matitac that now takes directories

performance data for basic_1 on dev.helm

with matita 0.99.2 we can validate lambdadelta_1 (as is) in 4 minutes

legacy_1, ground_1, and basic_1 recommitted without anticipation
this seems to be the fastest solution for now

updated  bibliography for text J1

- new naming sheme for documentation yields more stable names
- update for document J2a

news update and some bugs fixed

basic_1: COMMIT COMPLETED
- component wf3
- additional files
basic_2: some corrections

components: pc1, pc3, ty3, csubt, ex1

components: sc3, csubc

components: nf2, sn3, ex2

components: arity, csuba

component: pr3

components: wcpr0 pr1 pr2

component: pr0

components: A asucc aplus leq llt aprem ex0

- update for helena 0.8.2 and related files
- updated bibliography

additional commit for version 0.8.2
- we add exportation of the kernel entities to coq 8
- coq indeed accepts our translation of the GdA !!
- some improvements in Makefile and README

components: G, next_plus, sty0, sty1

first article on lambdadelta version 3

components: subst1 csubst0 csubst1 fsubst0
we committed almost half of basic_1

components: subst csubv

components: subst0

components: clen lift1 drop1

components: clear getl cimp
if anticipated, getl/drop.ma causes "Out of mamory" in matitac

components cnt drop

some improvements in the anticipator
- we anticipate the terms to be matched
- we do not anticipate inner fixpoints because we turn them into constants when we generate Grafite for the ng_kernel

depend update

components C r flt app lift

- matitac: now directories are allowed as command line arguments
           all .ma files inside these directories are compiled
- basic_1: commit os sections tlt iso

- some improvements in the generation of terms
- basic_1: we commit sections s and tlist

- we generate the terms in anticipated form (the are easier to debug)
- basic_1: commit of section T

porting of basic_1 for the ng_kernel: first step ...

notation ast updated to comply with the toplevel let rec of ng_kernel

refactoring of \lambda\delta version 1 in matita

dependences update

dependences update

informational page on ground_1

basic_1: we separate theorems and lemmas as in basic_2
         the informational page is complete

update in web page for basic_1

- we add an informational page on \lambda\delta version 1 (core)
- web site update

lambdadelta_1: bugfix
Makefile: some improvements

infrastructure to browse lambdadelta_1 remotely

lambdadelta_1 updated with new part names

we restored the scripts of \lambda\delta version 1
(which are now available through \lambda\delta Web site)
by merging and updating all our (not broken) scripts

...

- xhtbl: minor improvement
- web site update
- static xhtml pages from lddl: updated trough ld_web infrastructure

last commit for helena 0.8.2
- a check was missing in the comparator
- new textual syntax for \lambda\delta "Version 4"
  (exp_math files updated accordingly)
- minor bug fixes (BrgOutput now uses the new alpha-conversion)

the corrected "Grundlagen" is online

lddl update with the disambiguated "grundlagen"

- bugfix is refreshed state of AutCrg: now we return a fresh state
- minor changes in the xml format
- some refactoring

removing some old files

finite lambda calculus

A compiling version

- bug fix in the RTM
- we can validate the Grundlagen in lambda-delta version 3

check removed

0.5.9 released

- we add the missing layer constraint on applicability condition
- trace levels refactoring

now type inclusion is correctly managed in the RTM

- we are moving from old (patched) management of sort inclusion
  to new (proper) one via \lambda\delta 3
- some refactoring
- omega.out: committed for reference
- Makefiles: some bugs fixed

- we removed a flag from the kernel status
- some renaming

- helena: the improved attribute system allows to export the sorts of Pi's
  Pi's of sort Prop are rendered as Forall's in the generated Matita script
- we updated the dtd accordingly