Zulip Chat Archive

Stream: general

Topic: import with open_locale


view this post on Zulip Kenny Lau (Apr 12 2020 at 06:27):

import data.list
open_locale classical

error:

file 'open_locale' not found in the LEAN_PATH

file 'classical' not found in the LEAN_PATH

invalid import: open_locale
could not resolve import: open_locale

invalid import: classical
could not resolve import: classical

view this post on Zulip Kenny Lau (Apr 12 2020 at 06:27):

@Mario Carneiro

view this post on Zulip Yury G. Kudryashov (Apr 12 2020 at 06:28):

You need something between import and open_locale

view this post on Zulip Yury G. Kudryashov (Apr 12 2020 at 06:28):

AFAIR, a comment will do.

view this post on Zulip Yury G. Kudryashov (Apr 12 2020 at 06:28):

There can be no user-defined command after import

view this post on Zulip Kenny Lau (Apr 12 2020 at 06:32):

comments don't solve this

view this post on Zulip Kenny Lau (Apr 12 2020 at 06:32):

so I settled with #check id

view this post on Zulip Yury G. Kudryashov (Apr 12 2020 at 06:36):

Including /-! ... -/?

view this post on Zulip Kenny Lau (Apr 12 2020 at 06:36):

oh I didn't know that it exists

view this post on Zulip Yury G. Kudryashov (Apr 12 2020 at 06:40):

It is used for module-level docstrings

view this post on Zulip Mario Carneiro (Apr 12 2020 at 06:41):

I usually use section end

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 07:05):

I think /-! -/ is pretty golfy

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:07):

I worry about other options that they will affect the output

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:07):

for example does that leave something funny in the leandoc?

view this post on Zulip Kenny Lau (Apr 12 2020 at 07:07):

let's say the solution is universes u v

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:08):

that's not bad, although you might not want to declare universes

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:09):

aha, variables works

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:09):

import tactic.lint
variables
#lint

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 07:09):

I've seen someone use something like tactic.cmd skip or something, but I can never remember the syntax

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:10):

most plural commands like universes require 1 or more names

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:10):

but apparently variables is okay with 0

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:11):

I guess you mean run_cmd tactic.skip

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 07:11):

The elephant in the room: can this actually be fixed?

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:11):

It's a grammar definition problem

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 07:12):

Yeah but can it actually be fixed?

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:12):

That is, unless you change the lean grammar it is doing exactly what it should be doing

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 07:12):

Yeah but can it actually be fixed?

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:12):

My preferred solution is to allow . at the end of an import statement to end it

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:13):

We could do something like stop at newlines but that's a bit hackish

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:14):

plus it would have to be unindented lines since imports are sometimes formatted like

import foo bar
  baz
  quux

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:16):

Another possibility: since #lint is not a valid identifier (because of the hash), we can stop when we see something that isn't a name. This won't work for all user commands though; some of them are just words like alias

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 07:30):

I just don't understand why import data.real.basic followed by def x := ... works but you can't follow it by open_locale.

view this post on Zulip Yury G. Kudryashov (Apr 12 2020 at 07:34):

open_locale is a user-defined command.

view this post on Zulip Yury G. Kudryashov (Apr 12 2020 at 07:35):

It is defined in one of the imports

view this post on Zulip Yury G. Kudryashov (Apr 12 2020 at 07:35):

And I think that Lean doesn't start looking into these imports before parsing till the end of import list.

view this post on Zulip Yury G. Kudryashov (Apr 12 2020 at 07:36):

How should it know that you're not trying to import a file named 'open_locale'?

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 07:44):

How should it know that I'm not trying to import a file named def?

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 07:45):

You're talking about technicalities. I just don't understand why the problem can't be solved.

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:46):

A number of words like def, import, variables etc are reserved as "command keywords". You can write these anywhere in the file and lean will stop whatever it is doing and begin a new command

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:46):

this is why you can't have a tactic called set_option

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:47):

These define the high level structure of the lean file, and are about the only thing you can parse with no context

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 07:47):

I'm well aware that it doesn't currently work but what I'm saying is why can't it be fixed? That's what I don't understand

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:47):

The problem with user commands is that they are command keywords that require context

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 07:48):

Why not just add open_locale to some list

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:48):

If open_locale was built into lean, yes that would work

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:48):

but then it wouldn't be a user command

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 07:48):

So why can't we just build it into Lean?

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:49):

The point is that lean needs to know that this is a command before it's even read anything

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:49):

because it's a mathlib command

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 07:49):

So def is a command and open_locale is a user command?

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:49):

yes

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:49):

it's a command that was defined in a lean file rather than in C++

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 07:50):

What are the other user commands?

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:50):

#lint, alias, open_locale, a few others I'm sure

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:50):

you can grep for @[user_command]

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 07:50):

#find?

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:50):

yes

view this post on Zulip Bryan Gin-ge Chen (Apr 12 2020 at 07:51):

There's a more or less complete list here: https://leanprover-community.github.io/mathlib_docs/commands.html

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 07:51):

And we can't just add these to some list in core lean and say "this is a command which we'll define later"?

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:51):

we could, but that's not being nice to people who write their own user commands and want the same level of support

view this post on Zulip Mario Carneiro (Apr 12 2020 at 07:52):

the whole point of user commands is that they are not built in

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 07:52):

I see

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 07:52):

Now I can see the appeal of the full stop after imports over approach

view this post on Zulip Kenny Lau (Apr 12 2020 at 07:53):

btw fintype with open_locale classical is frustratingly slow

view this post on Zulip Kenny Lau (Apr 12 2020 at 07:54):

although I'm not sure if open_locale classical is the root cause

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 07:55):

We can't make it #open_locale and then tell lean that if it begins with a # then no way is it an import?

view this post on Zulip Kenny Lau (Apr 12 2020 at 08:23):

@Mario Carneiro is there a way to make Lean tell me which typeclass it struggles to resolve?

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:23):

@Kevin Buzzard We can, that's one of the options I mentioned

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:25):

but does it mean we have to put # on all user commands? I believe the intended meaning of # is temporary commands for interactive use, while several user commands are not meant to be temporary, such as alias, open_locale, add_decl_doc and others

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:26):

@Kenny Lau You can print out the typeclass search using set_option trace.class_instances true; the hard ones are the ones that print out megabytes of tracing info

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 08:27):

So maybe we come up with some other symbol to start a user command. How about ,?

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 08:27):

I've heard they're phasing it out in Lean 4 so it's probably going spare.

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:27):

Everything is in use by lean or coveted by mathematicians

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 08:28):

How about an emoji?

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:28):

that's probably a legal identifier character

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 08:28):

so is the d in def

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:29):

but once lean parses the word it finds it on its list of command keywords

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:29):

it won't find a user command on that list so it assumes it's a file name

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 08:30):

Ok so I don't feel too bad about banning file names which start with an emoji

view this post on Zulip Kenny Lau (Apr 12 2020 at 08:31):

@Mario Carneiro can I set_option class.instance_max_depth 10 with the same effect?

view this post on Zulip Kenny Lau (Apr 12 2020 at 08:31):

(the ones that fail to resolve are the problematic ones)

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:31):

YMMV

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:31):

try it and see

view this post on Zulip Kenny Lau (Apr 12 2020 at 08:32):

it can't work out that a group has multiplication

view this post on Zulip Gabriel Ebner (Apr 12 2020 at 08:33):

How about parsing indentation-sensitively, like Lean 4:

import foo
  bar
open_locale classical -- runs user command

and

import foo
  bar
 open_locale classical -- imports open_locale and classical modules

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:33):

@Kenny Lau You should probably ask a separate question, this is getting cluttered

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 08:34):

The indentation idea is by far the most practical I've heard so far

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:34):

I'm okay with the indentation solution because it will have a basically 100% success rate without any change to mathlib, although it would be a departure from anything we have done in lean parsing elsewhere

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:35):

I would prefer that we support both that and the . option

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:35):

for those who don't like indentation sensitivity

view this post on Zulip Gabriel Ebner (Apr 12 2020 at 09:26):

lean#188


Last updated: May 16 2021 at 05:21 UTC