on add_decl

Stream: general

[Johan Commelin]

I am trying to understand how to_additive works. This led me to add_decl. I'm confused about the following:

namespace tactic

meta def my_new_decl (src_name : name) : command :=
do env ←    get_env,
   decl ←   env.get src_name,
   let decl := decl.update_name $ `xyzzyquux,
   let decl := decl.update_type $ decl.type,
   let decl := decl.update_value $ decl.value,
   add_decl decl

run_cmd my_new_decl `has_mul

#print xyzzyquux
-- constant xyzzyquux : Type u → Type u

#print has_mul
/-
@[class, to_additive name.mk_string "has_add" name.anonymous]
structure has_mul : Type u → Type u
fields:
has_mul.mul : Π {α : Type u} [c : has_mul α], α → α → α
-/
end tactic

[Johan Commelin]

Why doesn't #print xyzzyquux give me a structure with fields?

[Chris Hughes]

If you look at the constructors to declaration, inductive is not an option. has_add is a constant. I guess you probably want tactic.add_inductive

[Johan Commelin]

Aha, let me take a look at that.

[Johan Commelin]

But how is to_additive doing this? I thought I had drilled down to the bottom when I hit add_decl. Did I miss a branch?

[Chris Hughes]

I don't think to_additive makes any new structures

[Mario Carneiro]

the lean metaprogramming stuff is not good at creating inductives

[Mario Carneiro]

there is a patch in the fork

[Mario Carneiro]

but on stock lean, you have to do a whole bunch of to_additive things around each new structure

[Mario Carneiro]

https://github.com/leanprover-community/mathlib/blob/master/src/algebra/group.lean#L636-L645

[Johan Commelin]

Ok, so the fork has happened...

[Johan Commelin]

But nobody is using it?

[Mario Carneiro]

right now it's just accumulating fixes

[Johan Commelin]

/- Add a new inductive datatype to the environment
   name, universe parameters, number of parameters, type, constructors (name and type), is_meta -/
meta def add_inductive (n : name) (ls : list name) (p : nat) (ty : expr) (is : list (name × expr))
  (is_meta : bool := ff) : tactic unit :=
updateex_env $ λe, e.add_inductive n ls p ty is is_meta

Can someone explain how to turn (ls : list name) into list of universe parameters?

[Johan Commelin]

I want just 1 universe

[Mario Carneiro]

we want to have a proper release at some point (see the tracking issue)

[Johan Commelin]

And my type will be Type (u + 1), for the corresponding u

[Mario Carneiro]

and if mathlib moves to the fork I'm sure development will accelerate

[Mario Carneiro]

Don't use add_inductive. It works only for the loosest definition of "works"

[Johan Commelin]

So what should I use?

[Johan Commelin]

The fork?

[Mario Carneiro]

yes, that's the patch I mentioned

[Scott Morrison]

Keeley has a (completely evil) trick for just emitting plain text for Lean to parse. So if you're desperate you can make inductive definitions programmatically using that. :-)

[Mario Carneiro]

another workaround that works on stock lean is to produce a string that looks like an inductive declaration and parse it into the environment

[Mario Carneiro]

what Scott said

[Johan Commelin]

Hmmm... I will have to think about what I want to do then

[Johan Commelin]

Switching a custom project to the fork should be easy, right?

[Mario Carneiro]

I think so... I'm not up on elan support

[Mario Carneiro]

I know Keeley and Ed have played with lean forks, they will know better

[Johan Commelin]

@Scott Morrison Do you know what I should put in my toml?

[Scott Morrison]

Where does the fork live?

[Johan Commelin]

https://github.com/leanprover-community/lean

[Mario Carneiro]

None of the PRs have actually been merged though, so master is still stock

[Mario Carneiro]

someone needs to work out why all the travis builds are failing

[Scott Morrison]

I think you can just write lean_version = "leanprover-community/lean:BRANCH" in your leanpkg.toml.

[Scott Morrison]

hmm, maybe not

[Mario Carneiro]

The relevant branch is https://github.com/leanprover-community/lean/pull/3

[Scott Morrison]

Oh, someone needs to actually run something to make the build that elan pulls, and I've never done that.

[Scott Morrison]

@Keeley Hoek?

[Johan Commelin]

Hmmm... I can't yet get it to work

[Keeley Hoek]

This works for me: https://github.com/khoek/leancache/blob/master/leanpkg.toml

[Keeley Hoek]

I haven't read this thread but have you guys made a release

[Johan Commelin]

khoek/klean:3.4.7 ... does that refer to a branch or a release?

[Keeley Hoek]

ohhh hang on, unless elan has been changed it doesn't pull from travis?

[Keeley Hoek]

It pulls from https://github.com/leanprover-community/lean/releases

[Keeley Hoek]

Pulling from travis would be a great feature....

[Johan Commelin]

Aaah... sure. I currently don't have the time to setup the build toolchain

[Johan Commelin]

So using the fork will have to wait.

[Keeley Hoek]

So for completeness, the syntax is user/repo:releasename where releasename is not a branch, but rather the name of the release on github without a "v" prepended (this was Leo's format).
e.g. leanprover/lean:3.4.2, where the github release is v3.4.2

[Keeley Hoek]

@Mario Carneiro It's alive! I would super duper like to merge two teeny functions which save and load exprs from disk using the C++ serializer/deserializer

[Keeley Hoek]

I think it could be lifechanging for people who modify core mathlib stuff like e.g. tactic.basic

[Mario Carneiro]

If you can figure out why travis is failing, I'll merge it

[Mario Carneiro]

I think that more olean metaprogramming access would be a very useful thing

[Keeley Hoek]

On it :D

[Keeley Hoek]

@Mario Carneiro Works now

[Keeley Hoek]

let me set up a fork

[Keeley Hoek]

(As in, whole thing builds on my machine)

[Johan Commelin]

another workaround that works on stock lean is to produce a string that looks like an inductive declaration and parse it into the environment

What Lean function is this?

[Simon Hudon]

In mathlib, it's called emit_code_here

[Simon Hudon]

it's in tactic.basic

[Simon Hudon]

There's a catch though. It's not a tactic. It's a parser command

[Simon Hudon]

That means that you can't invoke it in a tactic, you can only do it in the parser. For example, if you use @[user_command], this is something you can use.

[Johan Commelin]

Does Lean know that classX extends classY? Or is the only way to approximate this, by checking whether the environment contains classX.to_classY?