## Stream: general

#### Johan Commelin (Apr 08 2019 at 12:04):

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 (Apr 08 2019 at 12:04): Why doesn't #print xyzzyquux give me a structure with fields? #### Chris Hughes (Apr 08 2019 at 12:17): 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 (Apr 08 2019 at 12:22): Aha, let me take a look at that. #### Johan Commelin (Apr 08 2019 at 12:24): 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 (Apr 08 2019 at 12:25): I don't think to_additive makes any new structures #### Mario Carneiro (Apr 08 2019 at 12:26): the lean metaprogramming stuff is not good at creating inductives #### Mario Carneiro (Apr 08 2019 at 12:26): there is a patch in the fork #### Mario Carneiro (Apr 08 2019 at 12:27): but on stock lean, you have to do a whole bunch of to_additive things around each new structure #### Mario Carneiro (Apr 08 2019 at 12:30): https://github.com/leanprover-community/mathlib/blob/master/src/algebra/group.lean#L636-L645 #### Johan Commelin (Apr 08 2019 at 12:31): Ok, so the fork has happened... #### Johan Commelin (Apr 08 2019 at 12:31): But nobody is using it? #### Mario Carneiro (Apr 08 2019 at 12:36): right now it's just accumulating fixes #### Johan Commelin (Apr 08 2019 at 12:37): /- 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 (Apr 08 2019 at 12:37):

I want just 1 universe

#### Mario Carneiro (Apr 08 2019 at 12:37):

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

#### Johan Commelin (Apr 08 2019 at 12:37):

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

#### Mario Carneiro (Apr 08 2019 at 12:37):

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

#### Mario Carneiro (Apr 08 2019 at 12:38):

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

#### Johan Commelin (Apr 08 2019 at 12:39):

So what should I use?

The fork?

#### Mario Carneiro (Apr 08 2019 at 12:39):

yes, that's the patch I mentioned

#### Scott Morrison (Apr 08 2019 at 12:40):

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 (Apr 08 2019 at 12:40):

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 Scott said

#### Johan Commelin (Apr 08 2019 at 12:41):

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

#### Johan Commelin (Apr 08 2019 at 12:41):

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

#### Mario Carneiro (Apr 08 2019 at 12:41):

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

#### Mario Carneiro (Apr 08 2019 at 12:42):

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

#### Johan Commelin (Apr 08 2019 at 12:43):

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

#### Scott Morrison (Apr 08 2019 at 12:44):

Where does the fork live?

#### Johan Commelin (Apr 08 2019 at 12:44):

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

#### Mario Carneiro (Apr 08 2019 at 12:47):

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

#### Mario Carneiro (Apr 08 2019 at 12:47):

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

#### Scott Morrison (Apr 08 2019 at 12:48):

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

hmm, maybe not

#### Mario Carneiro (Apr 08 2019 at 12:50):

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

#### Scott Morrison (Apr 08 2019 at 12:53):

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

@Keeley Hoek?

#### Johan Commelin (Apr 08 2019 at 12:54):

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

#### Keeley Hoek (Apr 08 2019 at 12:54):

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

#### Johan Commelin (Apr 08 2019 at 12:56):

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

#### Keeley Hoek (Apr 08 2019 at 12:56):

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

#### Keeley Hoek (Apr 08 2019 at 12:57):

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

#### Johan Commelin (Apr 08 2019 at 13:00):

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

#### Johan Commelin (Apr 08 2019 at 13:00):

So using the fork will have to wait.

#### Keeley Hoek (Apr 08 2019 at 13:00):

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 (Apr 08 2019 at 13:01):

@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 (Apr 08 2019 at 13:02):

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

#### Mario Carneiro (Apr 08 2019 at 13:02):

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

#### Mario Carneiro (Apr 08 2019 at 13:03):

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

On it :D

#### Keeley Hoek (Apr 08 2019 at 13:18):

@Mario Carneiro Works now

#### Keeley Hoek (Apr 08 2019 at 13:18):

let me set up a fork

#### Keeley Hoek (Apr 08 2019 at 13:18):

(As in, whole thing builds on my machine)

#### Johan Commelin (Apr 08 2019 at 16:43):

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 (Apr 08 2019 at 17:17):

In mathlib, it's called emit_code_here

#### Simon Hudon (Apr 08 2019 at 17:17):

it's in tactic.basic

#### Simon Hudon (Apr 08 2019 at 17:18):

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

#### Simon Hudon (Apr 08 2019 at 17:21):

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 (Apr 08 2019 at 17:41):

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

Last updated: May 16 2021 at 22:14 UTC