]> matita.cs.unibo.it Git - helm.git/log
helm.git
17 years agoUpdated, proofs are now about 750 lines.
Wilmer Ricciotti [Wed, 12 Sep 2007 14:30:28 +0000 (14:30 +0000)]
Updated, proofs are now about 750 lines.

17 years agolibrarySync - we do not generate the object attributes when we publish the xml
Ferruccio Guidi [Tue, 11 Sep 2007 16:50:12 +0000 (16:50 +0000)]
librarySync - we do not generate the object attributes when we publish the xml
LambdaDelta-1 - new cast type rule

17 years agosome theorem names changed.
Cristian Armentano [Tue, 11 Sep 2007 14:25:35 +0000 (14:25 +0000)]
some theorem names changed.

17 years agoreplaced an assert false that cause nat_ind not to be displayed with a dummy result
Enrico Tassi [Tue, 11 Sep 2007 08:16:25 +0000 (08:16 +0000)]
replaced an assert false that cause nat_ind not to be displayed with a dummy result

17 years agolast version with caml 3.09 built and saved as 0.3.0
Enrico Tassi [Mon, 10 Sep 2007 18:35:11 +0000 (18:35 +0000)]
last version with caml 3.09 built and saved as 0.3.0

17 years ago...
Enrico Tassi [Mon, 10 Sep 2007 18:34:12 +0000 (18:34 +0000)]
...

17 years agoother simplifications.
Cristian Armentano [Mon, 10 Sep 2007 11:20:29 +0000 (11:20 +0000)]
other simplifications.

17 years agoThis test shows one of the few cases were Matita is able to infer a dependent
Claudio Sacerdoti Coen [Mon, 10 Sep 2007 08:34:41 +0000 (08:34 +0000)]
This test shows one of the few cases were Matita is able to infer a dependent
type. It should break if the dependent type is no longer inferred.

17 years ago* debian/control
Stefano Zacchiroli [Sun, 9 Sep 2007 21:25:58 +0000 (21:25 +0000)]
* debian/control
  - add XS-Vcs-* fields pointing to HELM's repository and browser

17 years ago...
Enrico Tassi [Sun, 9 Sep 2007 19:00:57 +0000 (19:00 +0000)]
...

17 years agoin the case of coerce_to_sort the whd was done with delta:true, that caused an incred...
Enrico Tassi [Sun, 9 Sep 2007 15:16:46 +0000 (15:16 +0000)]
in the case of coerce_to_sort the whd was done with delta:true, that caused an incredible slowdown in dama/
more debug printings added and some comments for vim folding mechanism

17 years agoother simplifications.
Cristian Armentano [Sun, 9 Sep 2007 13:45:27 +0000 (13:45 +0000)]
other simplifications.

17 years ago* NOT RELEASED YET
Stefano Zacchiroli [Sun, 9 Sep 2007 10:38:10 +0000 (10:38 +0000)]
* NOT RELEASED YET

17 years ago* change how the ocamldoc API reference is generated: no longer use upstream
Stefano Zacchiroli [Sun, 9 Sep 2007 10:36:04 +0000 (10:36 +0000)]
* change how the ocamldoc API reference is generated: no longer use upstream
  Makefile, but rather rely on CDBS
* debian/control
  - remove build-dep on texlive stuff and graphviz since now we only ship
    HTML version of the API reference
* debian/docs, debian/doc-base
  - file removed, the latter will be now automatically generated, the former
    would only contain README and CDBS is smart enough to guess it

17 years agohuge commit regarding coercions to funclass and eat_prods. before there was a
Enrico Tassi [Sat, 8 Sep 2007 23:50:41 +0000 (23:50 +0000)]
huge commit regarding coercions to funclass and eat_prods.  before there was a
so broken behaviour that is impossible to describe the changes.

now:
  eat_prods he hety args

  starts checking if hety is metaclosed, if it is does nothing, if not
  unifies it with ?->?-> ... ->? s.t. there is a Pi for every args.
  if this unification fails, does nothing (all coercions are in the
  second phase.

  continues eating prods in hety and args in parallel, if there is an arg
  and no more prods, tries to fix the arity of (he already_processed_args).
  fix_arity gives a range of possible coercions to funclass s.t.
  (c (he ..)) : FunType. The eat prods and args continues, eting the remaining
  args toghether with FunType. If it fails, it continues with another c to
  another FunType. This recursively (yes, it backtracks. no strong opinion
  here, but there is no sane heuristinc to chose one FunType).

  the code is reduced to 1/3, but Localization of errors probably need fixing.

17 years agothe order of abstraction is now correct, but there is an orrible hack to make eq_OF_e...
Enrico Tassi [Sat, 8 Sep 2007 23:41:54 +0000 (23:41 +0000)]
the order of abstraction is now correct, but there is an orrible hack to make eq_OF_eq have the right type.

17 years agoremoved an assertion that makes no more sense to me
Enrico Tassi [Sat, 8 Sep 2007 23:41:11 +0000 (23:41 +0000)]
removed an assertion that makes no more sense to me

17 years agobetter debug printings
Enrico Tassi [Sat, 8 Sep 2007 23:40:46 +0000 (23:40 +0000)]
better debug printings

17 years agobetter test for church numerals
Enrico Tassi [Sat, 8 Sep 2007 23:40:19 +0000 (23:40 +0000)]
better test for church numerals

17 years agojust a Pcre expression fixed, nothing real
Enrico Tassi [Sat, 8 Sep 2007 23:36:51 +0000 (23:36 +0000)]
just a Pcre expression fixed, nothing real

17 years ago...
Enrico Tassi [Sat, 8 Sep 2007 22:58:03 +0000 (22:58 +0000)]
...

17 years agomatita can now safely start a matitac that will put metadata in the right db.
Enrico Tassi [Sat, 8 Sep 2007 17:22:34 +0000 (17:22 +0000)]
matita can now safely start a matitac that will put metadata in the right db.

17 years agoFull specification of find. Added notation for If_Then_Else. Probably a delta
Enrico Tassi [Sat, 8 Sep 2007 17:21:58 +0000 (17:21 +0000)]
Full specification of find. Added notation for If_Then_Else. Probably a delta
on t in the match the decides if it is the case to pass a coercion under a
match whould be nice.

17 years agobump version
Stefano Zacchiroli [Sat, 8 Sep 2007 10:17:22 +0000 (10:17 +0000)]
bump version

17 years agorelease
Stefano Zacchiroli [Sat, 8 Sep 2007 10:14:30 +0000 (10:14 +0000)]
release

17 years ago* add ocamldoc comments to .mli interface files
Stefano Zacchiroli [Sat, 8 Sep 2007 10:11:43 +0000 (10:11 +0000)]
* add ocamldoc comments to .mli interface files

17 years agoinclude also gdome2/ dir in the ocamldoc include path
Stefano Zacchiroli [Sat, 8 Sep 2007 10:05:32 +0000 (10:05 +0000)]
include also gdome2/ dir in the ocamldoc include path

17 years ago* debian/rules
Stefano Zacchiroli [Sat, 8 Sep 2007 10:04:55 +0000 (10:04 +0000)]
* debian/rules
  - add additional flags for ocamldoc using "+=" instead of "=" ...

17 years agowhy the heck configure was committed?
Stefano Zacchiroli [Sat, 8 Sep 2007 09:57:44 +0000 (09:57 +0000)]
why the heck configure was committed?

17 years ago* debian/control
Stefano Zacchiroli [Sat, 8 Sep 2007 09:54:58 +0000 (09:54 +0000)]
* debian/control
  - port Vcs-Svn field to the new syntax
  - add XS-Vcs-Browser field pointing to HELM's repository browser
* debian/rules
  - enable ocamldoc api reference generation (via CDBS)

17 years agoinit new dummy entry
Stefano Zacchiroli [Sat, 8 Sep 2007 09:50:17 +0000 (09:50 +0000)]
init new dummy entry

17 years agoremove spurious comment
Stefano Zacchiroli [Sat, 8 Sep 2007 09:44:37 +0000 (09:44 +0000)]
remove spurious comment

17 years agoupload to unstable
Stefano Zacchiroli [Sat, 8 Sep 2007 09:42:13 +0000 (09:42 +0000)]
upload to unstable

17 years agoremove spurious entry
Stefano Zacchiroli [Sat, 8 Sep 2007 09:41:57 +0000 (09:41 +0000)]
remove spurious entry

17 years ago - s/Source-Version/binary:Version/ substvar
Stefano Zacchiroli [Sat, 8 Sep 2007 09:39:32 +0000 (09:39 +0000)]
  - s/Source-Version/binary:Version/ substvar

17 years agoadd stdlib/gdome2 to the include dir for ocamldoc
Stefano Zacchiroli [Sat, 8 Sep 2007 09:39:10 +0000 (09:39 +0000)]
add stdlib/gdome2 to the include dir for ocamldoc

17 years agobump version
Stefano Zacchiroli [Sat, 8 Sep 2007 09:30:29 +0000 (09:30 +0000)]
bump version

17 years ago* convert comments in .mli interface files to ocamldoc comments
Stefano Zacchiroli [Sat, 8 Sep 2007 09:27:43 +0000 (09:27 +0000)]
* convert comments in .mli interface files to ocamldoc comments
* bump debhelper compatibility level and dependency to 5
  - enable generation of ocamldoc api reference (via CDBS)
  - added XS-Vcs-* fields pointing to the svn repository
  - bumped build dependency on ocaml-nox to >= 3.10.0

17 years agoconvert comments to ocamldoc comments
Stefano Zacchiroli [Sat, 8 Sep 2007 09:16:29 +0000 (09:16 +0000)]
convert comments to ocamldoc comments

17 years ago1. fix_arity fixed: the code is totally wrong and this is just a quic&dirty
Enrico Tassi [Fri, 7 Sep 2007 17:58:54 +0000 (17:58 +0000)]
1. fix_arity fixed: the code is totally wrong and this is just a quic&dirty
   fix
2. first real-word example in coercions_russel: a certified "find" procedure
   from the ocaml library

Note: removing the (... : Prop) cast from the example, unification fails badly.
To be understood and fixed somehow (i.e. with an Uncertain in place of a
Failure).

17 years agoThis cast now works!
Enrico Tassi [Fri, 7 Sep 2007 15:48:52 +0000 (15:48 +0000)]
This cast now works!

 (λl:list nat. match l with [ nil ⇒ [] | cons x l1 ⇒ l1])
:
 ∀l:(∃l:list nat. l ≠ []). ∃l1.∃a.a :: l1 = l

17 years agowhen a coercion is passed through a case on right-params-free term m,
Enrico Tassi [Fri, 7 Sep 2007 15:46:51 +0000 (15:46 +0000)]
when a coercion is passed through a case on right-params-free term m,
branches and outtype are adjusted to receive an extra argument (refl m)
to have extra assumptions on it substituded. see tests/coercions_russell.ma

17 years agosome simplifications.
Cristian Armentano [Fri, 7 Sep 2007 14:10:46 +0000 (14:10 +0000)]
some simplifications.

17 years agoooops, missing )
Enrico Tassi [Fri, 7 Sep 2007 10:12:42 +0000 (10:12 +0000)]
ooops, missing )

17 years agodisabled coercions when refining paramod proofs (attemt to understand the slowdown...
Enrico Tassi [Fri, 7 Sep 2007 10:04:01 +0000 (10:04 +0000)]
disabled coercions when refining paramod proofs (attemt to understand the slowdown of night-tests)

17 years agofixed propagation under Fix/Lambda/Case of coercions, better names are
Enrico Tassi [Fri, 7 Sep 2007 09:59:52 +0000 (09:59 +0000)]
fixed propagation under Fix/Lambda/Case of coercions, better names are
generated.

there is still a question for CSC about the context of the metavariables opened
by example 51 that seems too long.

code still needs some refactoring, auxiliary functions are ready to be
lambdalifet out.

potential slowdown: The coerce_atom_to_something now looks for the *best*
coercion, where best means the one that opens the least number of metas.

17 years agoSome simplifications.
Cristian Armentano [Thu, 6 Sep 2007 15:17:56 +0000 (15:17 +0000)]
Some simplifications.

17 years agocoercions under Fix and Case. Code refactoring needed
Enrico Tassi [Thu, 6 Sep 2007 13:11:17 +0000 (13:11 +0000)]
coercions under Fix and Case. Code refactoring needed

17 years agoadded a duplicated implementation of replace lifting
Enrico Tassi [Thu, 6 Sep 2007 13:01:59 +0000 (13:01 +0000)]
added a duplicated implementation of replace lifting

17 years ago...
Enrico Tassi [Thu, 6 Sep 2007 13:00:58 +0000 (13:00 +0000)]
...

17 years ago- lybrarySync:
Ferruccio Guidi [Wed, 5 Sep 2007 19:29:10 +0000 (19:29 +0000)]
- lybrarySync:
  patched generation of published xml files: inner_sorts were not considered
- natitaInit:
  patched configuration parsing priority

17 years ago- matitaInit matitaprover matitadep matitamake:
Ferruccio Guidi [Wed, 5 Sep 2007 13:50:38 +0000 (13:50 +0000)]
- matitaInit matitaprover matitadep matitamake:
  fixed configuration precedence:
  cmdline > configuration_file > default
- core_natation:
  added notation for single step parallel reduction: =>
- LAMBDA-TYPES: some new theorems
- LOGIC: some new definitions

17 years agoadded fix case
Claudio Sacerdoti Coen [Wed, 5 Sep 2007 10:35:46 +0000 (10:35 +0000)]
added fix case

17 years agocoercions are propagated under Fix (but not mutually recursive Fixes)
Claudio Sacerdoti Coen [Wed, 5 Sep 2007 10:07:39 +0000 (10:07 +0000)]
coercions are propagated under Fix (but not mutually recursive Fixes)

17 years agoDandling ")" removed from notation for 'exists.
Claudio Sacerdoti Coen [Tue, 4 Sep 2007 12:21:40 +0000 (12:21 +0000)]
Dandling ")" removed from notation for 'exists.

17 years agoComposition of coercions with arity > 0 is now implemented correctly.
Claudio Sacerdoti Coen [Tue, 4 Sep 2007 10:45:18 +0000 (10:45 +0000)]
Composition of coercions with arity > 0 is now implemented correctly.

17 years agoA test for propagation of coercions (that open new goals) under lambdas,
Claudio Sacerdoti Coen [Tue, 4 Sep 2007 09:42:39 +0000 (09:42 +0000)]
A test for propagation of coercions (that open new goals) under lambdas,
cases, etc.

17 years ago1. composition of coercions with saturations > 0 is now implemented
Claudio Sacerdoti Coen [Tue, 4 Sep 2007 09:39:56 +0000 (09:39 +0000)]
1. composition of coercions with saturations > 0 is now implemented
2. as a side effect, there is no longer any difference between composition
   of coercions and the compose tactic

TODO: composition of coercions having arity > 0 is not implemented yet

17 years agoalpha conversion to avoid case-insensitivity of MySql on my laptop.
Claudio Sacerdoti Coen [Fri, 31 Aug 2007 09:07:19 +0000 (09:07 +0000)]
alpha conversion to avoid case-insensitivity of MySql on my laptop.
OK, I know, I should fix it...

17 years agobaseuri changed
Claudio Sacerdoti Coen [Fri, 31 Aug 2007 09:00:19 +0000 (09:00 +0000)]
baseuri changed

17 years agofixed coercions between arrows when the arrow is dependent.
Enrico Tassi [Fri, 31 Aug 2007 08:44:56 +0000 (08:44 +0000)]
fixed coercions between arrows when the arrow is dependent.

17 years agocaptured exception preserved (was replaced blindly with a RefineFailure)
Enrico Tassi [Thu, 30 Aug 2007 16:47:15 +0000 (16:47 +0000)]
captured exception preserved (was replaced blindly with a RefineFailure)

17 years agoreverted assertion, since it may happen to look for a coercion to funclass
Enrico Tassi [Thu, 30 Aug 2007 16:46:19 +0000 (16:46 +0000)]
reverted assertion, since it may happen to look for a coercion to funclass
even outside fix_arity (in cicRefine/eat_prods)

17 years agorefactoring of all coercions code and add a check to not perform a coercion check...
Enrico Tassi [Thu, 30 Aug 2007 16:25:17 +0000 (16:25 +0000)]
refactoring of all coercions code and add a check to not perform a coercion check if it is not needed

17 years agobugfix in computation of src and tgt for coercions with arity > 0
Enrico Tassi [Thu, 30 Aug 2007 16:24:31 +0000 (16:24 +0000)]
bugfix in computation of src and tgt for coercions with arity > 0

17 years agotests for coercions under lambdas
Enrico Tassi [Thu, 30 Aug 2007 13:39:33 +0000 (13:39 +0000)]
tests for coercions under lambdas

17 years agoCoercions are now generalized to the general form
Claudio Sacerdoti Coen [Thu, 30 Aug 2007 13:36:44 +0000 (13:36 +0000)]
Coercions are now generalized to the general form
f: \forall xs:Ts. \forall a:A xs. \forall ys:Ts'. B xs a ys
where f is declared as a coercion from A ? to B ? ? ? using the syntax

   coercion uri arity saturations

where:
 1. arity and saturations are optional with default 0
 2. the saturations option is the number of ys

Useful example: it is now possible to declare a coercion from
 nat to \exists n:nat. 0 \leq n
obtaining something extremely close to Russel (the new implementation of
the Program tactic of Coq) up to the fact that coercions are not propagated
yet under mutcases and fixes.

TODO: composition of coercions having saturations <> 0 is not implemented
yet (but should be easy to do, at least on paper)

17 years agoCoercions rework:
Enrico Tassi [Thu, 30 Aug 2007 13:24:13 +0000 (13:24 +0000)]
Coercions rework:
- new functions:
  - coerce_to_sort
  - coerce_to_something
  - coerce_atom_to_something
- added call in Cast
- coerce_to_something goes under lambdas in both
  variant and contravarian positions, to if there are
  c1: B -> B1 and c2:A1 -> C coercions, you can cast a function
  f: A -> B to A1 -> B1.

17 years agocoercions from funclass are not supported
Enrico Tassi [Thu, 30 Aug 2007 13:13:56 +0000 (13:13 +0000)]
coercions from funclass are not supported

17 years ago...
Enrico Tassi [Thu, 30 Aug 2007 13:13:14 +0000 (13:13 +0000)]
...

17 years agobla bla bla fallback
Enrico Tassi [Thu, 30 Aug 2007 13:12:37 +0000 (13:12 +0000)]
bla bla bla fallback

17 years agoadded a binch of svn:ignore
Enrico Tassi [Thu, 30 Aug 2007 13:11:59 +0000 (13:11 +0000)]
added a binch of svn:ignore

17 years agoadd a fallback in case the binaries are in the path and not in the runtime base dir
Enrico Tassi [Thu, 30 Aug 2007 13:11:24 +0000 (13:11 +0000)]
add a fallback in case the binaries are in the path and not in the runtime base dir

17 years agoprint few more wired assertions
Enrico Tassi [Thu, 30 Aug 2007 13:10:22 +0000 (13:10 +0000)]
print few more wired assertions

17 years agothe version on the livecd
Enrico Tassi [Thu, 30 Aug 2007 13:10:08 +0000 (13:10 +0000)]
the version on the livecd

17 years agomore stuff to reach an intensional definition of finite sets
Enrico Tassi [Thu, 30 Aug 2007 13:09:08 +0000 (13:09 +0000)]
more stuff to reach an intensional definition of finite sets

17 years agoadded an utility function
Enrico Tassi [Thu, 30 Aug 2007 13:08:24 +0000 (13:08 +0000)]
added an utility function

17 years ago0.2.0
Enrico Tassi [Thu, 30 Aug 2007 13:07:59 +0000 (13:07 +0000)]
0.2.0

17 years ago* definition of implication free propositional formulas
Claudio Sacerdoti Coen [Tue, 28 Aug 2007 15:32:32 +0000 (15:32 +0000)]
* definition of implication free propositional formulas
* definition of a classical semantics
* proofs of correctness of some syntactical manipulations to reach
  normal forms
* definition of sequent calculus trees
* proof of soundness of sequent calculus derivations
* proof of completeness of sequent calculus derivations (unfinished)

17 years agoA primer for Matita with some easy, medium, difficult and impossible exercises.
Claudio Sacerdoti Coen [Tue, 28 Aug 2007 15:27:01 +0000 (15:27 +0000)]
A primer for Matita with some easy, medium, difficult and impossible exercises.

17 years agoWe define proof tree tracks and normal proof tree tracks separately
Ferruccio Guidi [Sun, 26 Aug 2007 17:32:07 +0000 (17:32 +0000)]
We define proof tree tracks and normal proof tree tracks separately

17 years agorefactoring
Ferruccio Guidi [Sun, 26 Aug 2007 16:36:34 +0000 (16:36 +0000)]
refactoring

17 years agoproof by "introduction" (impi) implemented in full
Ferruccio Guidi [Sun, 26 Aug 2007 16:29:31 +0000 (16:29 +0000)]
proof by "introduction" (impi) implemented in full

17 years agothread-based interface activated again
Claudio Sacerdoti Coen [Sat, 25 Aug 2007 13:31:11 +0000 (13:31 +0000)]
thread-based interface activated again

17 years agoBug fixed: RewriteLR were not recognized correctly. Moreover they were also
Claudio Sacerdoti Coen [Thu, 23 Aug 2007 20:54:05 +0000 (20:54 +0000)]
Bug fixed: RewriteLR were not recognized correctly. Moreover they were also
handled incorrectly (according to the is_top_down flag that should be irrelevant).

17 years agoBug fixed: the initial metasenv used in the two tactic was empty!
Claudio Sacerdoti Coen [Thu, 23 Aug 2007 20:21:35 +0000 (20:21 +0000)]
Bug fixed: the initial metasenv used in the two tactic was empty!

17 years agoAvoid reusing Hbeta several times.
Claudio Sacerdoti Coen [Wed, 22 Aug 2007 09:39:34 +0000 (09:39 +0000)]
Avoid reusing Hbeta several times.

17 years agoselect now works correctly even if multiple hypotheses with the same name are
Claudio Sacerdoti Coen [Wed, 22 Aug 2007 08:14:21 +0000 (08:14 +0000)]
select now works correctly even if multiple hypotheses with the same name are
present in the context.

17 years agoAvoid confusion for names of proofs put in the applicative context.
Claudio Sacerdoti Coen [Tue, 21 Aug 2007 10:18:46 +0000 (10:18 +0000)]
Avoid confusion for names of proofs put in the applicative context.

17 years ago"obtain H E1=E2 by proof" is now working
Claudio Sacerdoti Coen [Tue, 21 Aug 2007 09:48:14 +0000 (09:48 +0000)]
"obtain H E1=E2 by proof" is now working

17 years agolittle change to theorem eq_gcd_times_times_eqv_times_gcd
Cristian Armentano [Thu, 16 Aug 2007 18:45:46 +0000 (18:45 +0000)]
little change to theorem eq_gcd_times_times_eqv_times_gcd

17 years agoremoved generic_sigma_p since generic_iter_p is the same
Andrea Asperti [Tue, 31 Jul 2007 11:18:35 +0000 (11:18 +0000)]
removed generic_sigma_p since generic_iter_p is the same

17 years agosomething was really too slow...
Enrico Tassi [Tue, 31 Jul 2007 10:40:30 +0000 (10:40 +0000)]
something was really too slow...

17 years agodefault equality stuff filtered out from hint rewrite
Enrico Tassi [Tue, 31 Jul 2007 10:39:53 +0000 (10:39 +0000)]
default equality stuff filtered out from hint rewrite

17 years agoremoved comments in proof presentation
Enrico Tassi [Tue, 31 Jul 2007 10:39:31 +0000 (10:39 +0000)]
removed comments in proof presentation

17 years agorenamed generic_sigma_p.ma to generic_iter_p.ma
Cristian Armentano [Mon, 30 Jul 2007 15:01:31 +0000 (15:01 +0000)]
renamed generic_sigma_p.ma to generic_iter_p.ma

17 years agoadded 'rewrite' option to the the hint macro. a cicBrowser with all library
Enrico Tassi [Mon, 30 Jul 2007 12:00:31 +0000 (12:00 +0000)]
added 'rewrite' option to the the hint macro. a cicBrowser with all library
objects that may rewrite the goal is displayed.

17 years agoWe add a binary for computing the "heights" of helm objects
Ferruccio Guidi [Thu, 26 Jul 2007 14:35:05 +0000 (14:35 +0000)]
We add a binary for computing the "heights" of helm objects
[this is related to the height of the dependece tree]

17 years agoadded development path normalization, inclusions with '../' in the path should now...
Enrico Tassi [Thu, 26 Jul 2007 13:47:07 +0000 (13:47 +0000)]
added development path normalization, inclusions with '../' in the path should now be handled correclty

17 years agoauto -> autobatch
Enrico Tassi [Thu, 26 Jul 2007 13:46:07 +0000 (13:46 +0000)]
auto -> autobatch