Zulip Chat Archive

Stream: general

Topic: on add_decl


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?

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

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

Mario Carneiro (Apr 08 2019 at 12:40):

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.

Scott Morrison (Apr 08 2019 at 12:49):

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.

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

@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

Keeley Hoek (Apr 08 2019 at 12:55):

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

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):

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

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

Keeley Hoek (Apr 08 2019 at 13:12):

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: Dec 20 2023 at 11:08 UTC