## Stream: new members

### Topic: DVRs

#### Johan Commelin (Jun 05 2020 at 20:06):

map_top' : to_fun 0 = 1 looks wrong...

#### Johan Commelin (Jun 05 2020 at 20:07):

You could decide to map 0 to something (I would choose 0, if you don't add infinity to Z). But then you need to exclude it in map_add_leq'.

#### Johan Commelin (Jun 05 2020 at 20:08):

@Ashvni Narayanan Where do you get your errors? Could you edit your message, to add a comment in the code saying -- error here?

#### Johan Commelin (Jun 05 2020 at 20:08):

max_ideal is not known, because the full name is discrete_valuation_ring.max_ideal.
You could write open discrete_valuation_ring if you want to get access to it.

#### Jalex Stark (Jun 05 2020 at 20:09):

when I try to run your code block, I get unknown identifier 'principal_ideal_domain' is there a missing open namespace?

#### Johan Commelin (Jun 05 2020 at 20:09):

Alternative: extend local_ring R as well... and then you only need uniq_prime_ideal

#### Johan Commelin (Jun 05 2020 at 20:10):

For the other error, my guess is that you need ideal.span ({\pi} : set R)

#### Patrick Massot (Jun 05 2020 at 20:10):

variables [discrete_valuation_ring R]
open discrete_valuation_ring
def uniformizers : set R := { π | ideal.span ({π} : set R) = max_ideal }


will probably help

#### Patrick Massot (Jun 05 2020 at 20:11):

The ({π} : set R)  is a shame, this is Lean 3 elaborator not being smart enough. The rest is on you.

#### Patrick Massot (Jun 05 2020 at 20:12):

And you probably want to define a version of max_ideal where R is explicit.

#### Patrick Massot (Jun 05 2020 at 20:12):

But that's up to you.

#### Johan Commelin (Jun 05 2020 at 20:13):

Well, you don't want it to conflict with local_ring. So you should reuse that.

#### Patrick Massot (Jun 05 2020 at 20:14):

Also, could you please edit your first message above to change the topic to something more useful? The whole stream is for noob questions so your simply repeating information instead of having your own cosy little topic.

#### Johan Commelin (Jun 05 2020 at 20:19):

@Ashvni Narayanan You need    (next to the 1 on qwerty keyboards).

#### Johan Commelin (Jun 05 2020 at 20:19):

@Ashvni Narayanan Anyway, I should say that it's cool to see you attacking DVRs

#### Ashvni Narayanan (Jun 06 2020 at 00:25):

Thank you all! It is now showing me the error

type mismatch at application
ideal.span {π} = max_ideal
term
max_ideal
has type
Π (R : Type ?) [c : discrete_valuation_ring R], ideal R : Type (?+1)
but is expected to have type
ideal R : Type u


I don't see why this type mismatch occurs, because both are in ideals in R..

#### Bryan Gin-ge Chen (Jun 06 2020 at 00:26):

The first type Π (R : Type ?) [c : discrete_valuation_ring R], ideal R : Type (?+1) cannot be unified with the second type ideal R : Type u. Do you see why?

#### Bryan Gin-ge Chen (Jun 06 2020 at 00:27):

I suspect max_ideal is missing an argument.

#### Ashvni Narayanan (Jun 06 2020 at 00:28):

I am guessing I should explicitly define the type of max_ideal?

#### Bryan Gin-ge Chen (Jun 06 2020 at 00:39):

import ring_theory.ideals
import ring_theory.principal_ideal_domain
import ring_theory.localization

universe u

class discrete_valuation_ring (R : Type u) extends principal_ideal_domain R :=
(max_ideal : ideal R)
(maximal : max_ideal.is_maximal)
(unique_prime_ideal : ∀ M : ideal R, M.is_prime → M = ⊥ ∨ M = max_ideal)

-- this doesn't work for me because fraction_ring was removed in a recent commit to mathlib:
-- structure discrete_valuation_ring.discrete_valuation (R : Type u) [discrete_valuation_ring R] extends localization.fraction_ring R →* ℤ :=
-- (map_top' : to_fun 0 = 1)
-- (map_add_leq' : ∀ x y, to_fun (x + y) ≤ max (to_fun x) (to_fun y))
variables {R : Type u} [discrete_valuation_ring R]
open discrete_valuation_ring
def uniformizers : set R := { π | ideal.span ({π} : set R) = max_ideal }  -- fixed


#### Bryan Gin-ge Chen (Jun 06 2020 at 00:41):

You don't have to give R as a parameter to discrete_valuation_ring.max_ideal. The discrete_valuation_ring structure on R is found via type class inference.

#### Ashvni Narayanan (Jun 07 2020 at 15:49):

Sorry, I'm not sure I understand. How do I define max_ideal without saying that it is an ideal of R? Perhaps I misunderstood.

#### Kevin Buzzard (Jun 07 2020 at 15:50):

Can you restate the problem, if there is still a problem?

#### Ashvni Narayanan (Jun 07 2020 at 15:52):

import ring_theory.ideals

import ring_theory.principal_ideal_domain

import ring_theory.localization

universe u

class discrete_valuation_ring (α : Type u) extends principal_ideal_domain α :=
(max_ideal : ideal α)
(maximal : max_ideal.is_maximal)
(unique_prime_ideal : ∀ M : ideal α, M.is_prime → M = ⊥ ∨ M = max_ideal)

structure discrete_valuation_ring.discrete_valuation (α : Type u) [discrete_valuation_ring α] extends localization.fraction_ring α →* ℤ :=

(map_top' : to_fun 0 = 1)

(map_add_leq' : ∀ x y, to_fun (x + y) ≤ max (to_fun x) (to_fun y))

variables (α : Type u) [discrete_valuation_ring α ]
open discrete_valuation_ring
def uniformizers := { π | ideal.span ({π} :set α ) = max_ideal }


The last line gives me an error :

type mismatch at application
ideal.span {π} = max_ideal
term
max_ideal
has type
Π (α : Type ?) [c : discrete_valuation_ring α], ideal α : Type (?+1)
but is expected to have type
ideal α : Type u


#### Kevin Buzzard (Jun 07 2020 at 15:52):

max_ideal is a function which eats two things, first R and second a proof that R is a DVR, and spits out the max ideal of R. Because R is in round brackets the user has to supply it themselves. Because the DVR parameter is in square brackets, Lean will supply it automatically.

#### Kevin Buzzard (Jun 07 2020 at 15:54):

wait, the error is elsewhere

#### Kevin Buzzard (Jun 07 2020 at 15:56):

Ashvni can you update your Lean to the current version? I don't get an error with the max_ideal, perhaps because I am a bit more up to date.

#### Kevin Buzzard (Jun 07 2020 at 15:56):

leanproject up should do it (then close and open VS Code, it should restore all the files you had open etc)

#### Bryan Gin-ge Chen (Jun 07 2020 at 15:58):

(You can also restart Lean without restarting VS Code by hitting ctrl+shift+P and searching for the "Lean: restart" command.)

#### Ashvni Narayanan (Jun 07 2020 at 16:01):

Still shows me the same error

#### Bryan Gin-ge Chen (Jun 07 2020 at 16:07):

That is strange. What does your leanpkg.toml say?

#### Kevin Buzzard (Jun 07 2020 at 16:07):

Did you update Lean and mathlib with leanproject up?

#### Ashvni Narayanan (Jun 07 2020 at 16:14):

No, I did Lean : restart. That did not work. Sorry, how do I update Lean using leanproject up?

#### Bryan Gin-ge Chen (Jun 07 2020 at 16:15):

leanproject up is a command you need to enter at the command line.

#### Bryan Gin-ge Chen (Jun 07 2020 at 16:16):

It should work if you followed the recommended directions at https://leanprover-community.github.io/get_started.html#regular-install

#### Kevin Buzzard (Jun 07 2020 at 16:16):

You have to run it in the directory of the project. It's the only trick you have to know about from the command line. It keeps your Lean and mathlib up to date so you have the latest tactics

#### Johan Commelin (Jun 07 2020 at 16:18):

As I've said before, I think you should extend local_ring R.

#### Kevin Buzzard (Jun 07 2020 at 16:21):

Can we just extend local_ring R and principal_ideal_domain R? That would then be the full definition, right? With old structure command true?

#### Kevin Buzzard (Jun 07 2020 at 16:22):

import ring_theory.ideals
import ring_theory.principal_ideal_domain
import ring_theory.localization

set_option old_structure_cmd true

class discrete_valuation_ring (R : Type*)
extends principal_ideal_domain R, local_ring R.


#### Kevin Buzzard (Jun 07 2020 at 16:23):

wait, that includes fields which are probably not DVRs

#### Kevin Buzzard (Jun 07 2020 at 16:25):

class discrete_valuation_ring (R : Type*)
extends principal_ideal_domain R, local_ring R :=
(non_field : local_ring.nonunits_ideal R ≠ ⊥)


? What should the structure field be called?

#### Kevin Buzzard (Jun 07 2020 at 16:27):

There's no local_ring.maximal_ideal?

#### Johan Commelin (Jun 07 2020 at 16:27):

I think local_ring.max_ideal should be an alias for nonunits_ideal

#### Johan Commelin (Jun 07 2020 at 16:27):

Or the latter should simply be renamed

#### Ashvni Narayanan (Jun 07 2020 at 19:15):

I tried to update with leanproject up, says command not found. Also, Lean is taking a really long time to check goals, and is now showing me 1001 errors. Maybe I should just reinstall Lean?

#### Johan Commelin (Jun 07 2020 at 19:18):

That shouldn't be necessary

#### Johan Commelin (Jun 07 2020 at 19:19):

@Ashvni Narayanan do you have elan installed?

#### Bryan Gin-ge Chen (Jun 07 2020 at 19:19):

How did you install Lean? The recommended instructions are at this link: #install

#### Ashvni Narayanan (Jun 07 2020 at 19:22):

I installed Lean a while ago, I am quite sure I followed the instructions. I don't think I have installed elan

#### Bryan Gin-ge Chen (Jun 07 2020 at 19:28):

The instructions include installing elan as one of the steps (and have for more than a year). Try going through the directions corresponding to the operating system you're using in the link above.

#### Johan Commelin (Jun 07 2020 at 19:29):

@Ashvni Narayanan In a terminal, could you run the command which lean?

#### Johan Commelin (Jun 07 2020 at 19:30):

If it says something that ends in .elan/bin/lean, then you have elan installed

#### Ashvni Narayanan (Jun 07 2020 at 19:30):

Yes, I do have elan installed.

#### Kevin Buzzard (Jun 07 2020 at 19:31):

Did you install lean when you did that project with Lambert about six months ago?

Yes

#### Johan Commelin (Jun 07 2020 at 19:31):

If you have elan, then leanproject up should not cause problems

#### Kevin Buzzard (Jun 07 2020 at 19:32):

She might not have leanproject

#### Kevin Buzzard (Jun 07 2020 at 19:32):

She might have followed the instructions exactly as they were before leanproject appeared

#### Johan Commelin (Jun 07 2020 at 19:33):

Aah, I see. @Ashvni Narayanan leanproject is a really useful tool. It will automatically download the latest version of mathlib, with precompiled binaries. So it exactly solves the problem of lean being very slow, and all those errors, etc...

#### Ashvni Narayanan (Jun 07 2020 at 19:36):

I see. I will try to install it.

#### Ashvni Narayanan (Jun 08 2020 at 11:56):

Installing leanproject didn't work out too well. The Lean checker was taking too long and was showing 1001 errors. So I uninstalled and reinstalled Lean. But the same thing continues. Also, when I try to use leanproject, I get :

[WinError 5] Access is denied: 'C:\\Users\\ashvn\\my_project\\_target\\deps\\mathlib\\.git\\objects\\04\\7707d4b8ad5af2062cd42ae6ea954fa9fdda62'


#### Johan Commelin (Jun 08 2020 at 12:02):

@Kenny Lau Didn't you have similar issues at some point?

#### Kevin Buzzard (Jun 08 2020 at 12:38):

What do you get if you type leanproject --version?

#### Kenny Lau (Jun 08 2020 at 13:20):

@Johan Commelin yeah and then Patrick fixed it

#### Ashvni Narayanan (Jun 08 2020 at 16:02):

leanproject, version 0.0.8


#### Kevin Buzzard (Jun 08 2020 at 17:58):

@Patrick Massot aargh

#### Patrick Massot (Jun 08 2020 at 18:02):

That's a new error, not the same as Kenny's.

#### Patrick Massot (Jun 08 2020 at 18:03):

Well, it's sort of the same error: a Windows user

#### Kevin Buzzard (Jun 08 2020 at 18:03):

So what's the workaround?

#### Patrick Massot (Jun 08 2020 at 18:03):

Installing Linux?

#### Kevin Buzzard (Jun 08 2020 at 18:04):

Is there anything which takes up fewer gigabytes of memory?

#### Patrick Massot (Jun 08 2020 at 18:04):

Before that maybe try with current leanproject master, since I changed stuff this morning.

#### Bryan Gin-ge Chen (Jun 08 2020 at 18:10):

I remember having to delete _target in an old Lean package on my Windows machine when I started using leanproject there. Maybe that will help?

#### Patrick Massot (Jun 08 2020 at 18:15):

This is worth trying.

#### Patrick Massot (Jun 08 2020 at 18:17):

This morning I was testing video conference with people that I'll interview for a job on Thursday. The first one couldn't hear what I was saying. After twenty minutes trying various stuff, he wrote he was using Windows. Not only he was using Windows, but he wasn't knowing the basics of using Windows. I had to write he should try rebooting his computer. And then it worked.

#### Kevin Buzzard (Jun 08 2020 at 18:27):

If only one could prove theorems this way

#### Johan Commelin (Jun 08 2020 at 18:28):

Did you ever try it?

#### Kevin Buzzard (Jun 08 2020 at 18:29):

I'm not on Windows so I tend not to reboot my computer

#### Patrick Massot (Jun 08 2020 at 18:31):

This is the kind of stories that tell me from time to time that nothing changed since I stopped using Windows in 1999.

#### Kevin Buzzard (Jun 08 2020 at 18:35):

@Ashvni Narayanan try removing the subdirectory _target from the root directory of your project, and then running leanproject up again

#### Ashvni Narayanan (Jun 08 2020 at 19:30):

It is finally working! Turns out my file was in the wrong location. Apologies for the bother!

#### Kevin Buzzard (Jun 08 2020 at 19:31):

Next time you want to talk about DVRs, start a chat in #maths because not everyone looks here

#### Johan Commelin (Jun 08 2020 at 19:31):

Congrats! It's a real pain, getting the setup right. But now you can finally start doing maths again...

#### Ashvni Narayanan (Jun 08 2020 at 19:32):

Thanks for all the help!

#### Patrick Massot (Jun 08 2020 at 19:33):

If you understand what you were doing wrong and have suggestions to improve the documentation then we're interested.

#### Ashvni Narayanan (Jun 08 2020 at 20:12):

The problem is back :

import ring_theory.localization


gives the error

invalid import: ring_theory.localization
excessive memory consumption detected at 'expression traversal' (potential solution: increase memory consumption threshold)


Also,

leanproject up


still does not work. This time, this is the error:

[WinError 5] Access is denied: 'C:\\Users\\ashvn\\my_project\\_target\\deps\\mathlib\\.git\\objects\\04\\7707d4b8ad5af2062cd42ae6ea954fa9fdda62'


I am totally clueless now.

#### Kevin Buzzard (Jun 08 2020 at 20:15):

Did you try closing VS Code and re-opening?

#### Kevin Buzzard (Jun 08 2020 at 20:16):

Sometimes things run out of memory, and restarting can fix it. The leanproject error is a different issue.

#### Ashvni Narayanan (Jun 08 2020 at 20:16):

I have restarted it a few times.

#### Kevin Buzzard (Jun 08 2020 at 20:17):

Can you send a screenshot? Did you "open folder" and open your project folder (if you just open a file, imports won't work)

#### Ashvni Narayanan (Jun 08 2020 at 20:21):

I restarted and tried again, got a different error.

#### Kevin Buzzard (Jun 08 2020 at 20:27):

You don't have any errors there, you have an orange bar.

#### Kevin Buzzard (Jun 08 2020 at 20:28):

The error is reporting what happened before you'd finished typing. Your problem is that you don't have a compiled mathlib. Please remove _target, upgrade leanproject and run leanproject up in the root directory of the project. And close VS Code, it's just making your computer hot.

#### Yakov Pechersky (Jun 08 2020 at 20:29):

In general, I've found leanproject up breaks my directories. You can try editing your leanpkg.toml to a more recent lean and mathlib dependencies, and then running leanpkg get-cache leanproject get-cache

#### Kevin Buzzard (Jun 08 2020 at 20:29):

Don't do this, it's not supported and for a beginner it will make matters worse

#### Kevin Buzzard (Jun 08 2020 at 20:29):

An expert can perhaps try this approach

#### Bryan Gin-ge Chen (Jun 08 2020 at 20:30):

Also, I think you mean leanproject get-cache, not leanpkg get-cache.

#### Kevin Buzzard (Jun 08 2020 at 20:31):

leanproject up shouldn't break anything, and if it's breaking something then rather than working around it you should file an issue. Who knows what Yakov means but we are trying to get a new user with little experience in the command line up and running, and starting to use deprecated commands is, for this user, a step in the wrong direction. I totally appreciate that there are other ways to do this.

#### Kevin Buzzard (Jun 08 2020 at 20:34):

@Ashvni Narayanan if on the command line, in the directory called my_project, what happens if you type lean --make DVR.lean? Do you get an error? Does the command succeed, or just sit there doing nothing?

#### Ashvni Narayanan (Jun 08 2020 at 20:41):

It does not show an error, I don't know if it is successful, some parsing seems to be happening

#### Kevin Buzzard (Jun 08 2020 at 20:41):

I think your problem is that you don't have a compiled Lean. Can you try updating leanproject to 0.0.9?

#### Kevin Buzzard (Jun 08 2020 at 20:42):

Just do what you did to install it -- it got updated today.

#### Kevin Buzzard (Jun 08 2020 at 20:43):

Then try, in your project, rm -rf _target and then leanproject up again. Do all of these with the command line in root directory of your project folder. You can check to see if the rm command worked by typing ls before and after -- before, ls should show a directory called _target but afterwards it should be gone

#### Bryan Gin-ge Chen (Jun 08 2020 at 20:43):

I don't think 0.0.9 has been released yet: https://pypi.org/project/mathlibtools/

#### Kevin Buzzard (Jun 08 2020 at 20:44):

Thanks Bryan. In that case, just try removing _target and seeing what happens.

#### Kevin Buzzard (Jun 08 2020 at 20:45):

If you get the same error about access is denied, I'll have to leave you in the hands of someone who understands Windows. @Yakov Pechersky can you suggest anything less drastic than editing leanpkg.toml? I really want this to be a last resort because it will be hard to explain

#### Yakov Pechersky (Jun 08 2020 at 20:46):

I would remove the entire directory using File Explorer, and start over with a leanproject get ...

#### Yakov Pechersky (Jun 08 2020 at 20:47):

and hope it works! What's the leanproject project name that is causing issues? I can try it on my windows machine

#### Kevin Buzzard (Jun 08 2020 at 20:48):

ha ha! Ashvni this is certainly another approach! Is the project you're working on on GitHub?

#### Kevin Buzzard (Jun 08 2020 at 20:50):

If not, then try leanproject new dvr-project and then copy stuff over. Perhaps this is the simplest solution.

#### Kevin Buzzard (Jun 08 2020 at 20:50):

Output should look something like this:

\$ leanproject new dvr_project
> mkdir -p dvr_project
> cd dvr_project
> mkdir src
> git init -q
> git checkout -b lean-3.4.2
Switched to a new branch 'lean-3.4.2'
configuring dvr_project 0.1
mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
> git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 290, done.
remote: Counting objects: 100% (290/290), done.
remote: Compressing objects: 100% (214/214), done.
remote: Total 51776 (delta 181), reused 130 (delta 74), pack-reused 51486
Receiving objects: 100% (51776/51776), 22.32 MiB | 1.07 MiB/s, done.
Resolving deltas: 100% (39965/39965), done.
> git checkout --detach 470ccd328e15391cf328e0e006e13a06ff7d7b29    # in directory _target/deps/mathlib
HEAD is now at 470ccd32 chore(scripts): update nolints.txt (#2993)
configuring dvr_project 0.1
mathlib: trying to update _target/deps/mathlib to revision 470ccd328e15391cf328e0e006e13a06ff7d7b29
> git checkout --detach 470ccd328e15391cf328e0e006e13a06ff7d7b29    # in directory _target/deps/mathlib
HEAD is now at 470ccd32 chore(scripts): update nolints.txt (#2993)
Looking for local mathlib oleans
Looking for remote mathlib oleans
100%|█████████████████████████████████████████████████████████████████████████████████████| 22.5M/22.5M [00:21<00:00, 1.07MiB/s]
Found mathlib oleans at https://oleanstorage.azureedge.net/mathlib/


#### Ashvni Narayanan (Jun 08 2020 at 20:50):

I tried removing target, and

leanproject up
`

worked. Currently, it shows 10 problems instead of 1001, so I assume things are working okay

#### Kevin Buzzard (Jun 08 2020 at 20:51):

rofl, working OK is 0 problems :D

#### Bryan Gin-ge Chen (Jun 08 2020 at 21:11):

Glad you got things working! I opened an issue: mathlib-tools#55

Last updated: May 06 2021 at 23:11 UTC