Zulip Chat Archive

Stream: new members

Topic: DVRs


view this post on Zulip Johan Commelin (Jun 05 2020 at 20:06):

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

view this post on Zulip 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'.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 05 2020 at 20:09):

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

view this post on Zulip Johan Commelin (Jun 05 2020 at 20:10):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 05 2020 at 20:12):

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

view this post on Zulip Patrick Massot (Jun 05 2020 at 20:12):

But that's up to you.

view this post on Zulip Johan Commelin (Jun 05 2020 at 20:13):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 05 2020 at 20:19):

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

view this post on Zulip Johan Commelin (Jun 05 2020 at 20:19):

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

view this post on Zulip 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..

view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Jun 06 2020 at 00:27):

I suspect max_ideal is missing an argument.

view this post on Zulip Ashvni Narayanan (Jun 06 2020 at 00:28):

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

view this post on Zulip 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:
-- https://github.com/leanprover-community/mathlib/commit/80ad9edc9a6d6d2971dd044f6079cc770e755020
-- 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 07 2020 at 15:50):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 07 2020 at 15:54):

wait, the error is elsewhere

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.)

view this post on Zulip Ashvni Narayanan (Jun 07 2020 at 16:01):

Still shows me the same error

view this post on Zulip Bryan Gin-ge Chen (Jun 07 2020 at 16:07):

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

view this post on Zulip Kevin Buzzard (Jun 07 2020 at 16:07):

Did you update Lean and mathlib with leanproject up?

view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Jun 07 2020 at 16:15):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 07 2020 at 16:18):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 07 2020 at 16:23):

wait, that includes fields which are probably not DVRs

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jun 07 2020 at 16:27):

There's no local_ring.maximal_ideal?

view this post on Zulip Johan Commelin (Jun 07 2020 at 16:27):

I think local_ring.max_ideal should be an alias for nonunits_ideal

view this post on Zulip Johan Commelin (Jun 07 2020 at 16:27):

Or the latter should simply be renamed

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 07 2020 at 19:18):

That shouldn't be necessary

view this post on Zulip Johan Commelin (Jun 07 2020 at 19:19):

@Ashvni Narayanan do you have elan installed?

view this post on Zulip Bryan Gin-ge Chen (Jun 07 2020 at 19:19):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 07 2020 at 19:29):

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

view this post on Zulip Johan Commelin (Jun 07 2020 at 19:30):

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

view this post on Zulip Ashvni Narayanan (Jun 07 2020 at 19:30):

Yes, I do have elan installed.

view this post on Zulip Kevin Buzzard (Jun 07 2020 at 19:31):

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

view this post on Zulip Ashvni Narayanan (Jun 07 2020 at 19:31):

Yes

view this post on Zulip Johan Commelin (Jun 07 2020 at 19:31):

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

view this post on Zulip Kevin Buzzard (Jun 07 2020 at 19:32):

She might not have leanproject

view this post on Zulip Kevin Buzzard (Jun 07 2020 at 19:32):

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

view this post on Zulip 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...

view this post on Zulip Ashvni Narayanan (Jun 07 2020 at 19:36):

I see. I will try to install it.

view this post on Zulip 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'

view this post on Zulip Johan Commelin (Jun 08 2020 at 12:02):

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

view this post on Zulip Kevin Buzzard (Jun 08 2020 at 12:38):

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

view this post on Zulip Kenny Lau (Jun 08 2020 at 13:20):

@Johan Commelin yeah and then Patrick fixed it

view this post on Zulip Ashvni Narayanan (Jun 08 2020 at 16:02):

leanproject, version 0.0.8

view this post on Zulip Kevin Buzzard (Jun 08 2020 at 17:58):

@Patrick Massot aargh

view this post on Zulip Patrick Massot (Jun 08 2020 at 18:02):

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

view this post on Zulip Patrick Massot (Jun 08 2020 at 18:03):

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

view this post on Zulip Kevin Buzzard (Jun 08 2020 at 18:03):

So what's the workaround?

view this post on Zulip Patrick Massot (Jun 08 2020 at 18:03):

Installing Linux?

view this post on Zulip Kevin Buzzard (Jun 08 2020 at 18:04):

Is there anything which takes up fewer gigabytes of memory?

view this post on Zulip Patrick Massot (Jun 08 2020 at 18:04):

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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jun 08 2020 at 18:15):

This is worth trying.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 08 2020 at 18:27):

If only one could prove theorems this way

view this post on Zulip Johan Commelin (Jun 08 2020 at 18:28):

Did you ever try it?

view this post on Zulip Kevin Buzzard (Jun 08 2020 at 18:29):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Ashvni Narayanan (Jun 08 2020 at 19:32):

Thanks for all the help!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 08 2020 at 20:15):

Did you try closing VS Code and re-opening?

view this post on Zulip 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.

view this post on Zulip Ashvni Narayanan (Jun 08 2020 at 20:16):

I have restarted it a few times.

view this post on Zulip 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)

view this post on Zulip Ashvni Narayanan (Jun 08 2020 at 20:21):

image.png

I restarted and tried again, got a different error.

view this post on Zulip Kevin Buzzard (Jun 08 2020 at 20:27):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 08 2020 at 20:29):

An expert can perhaps try this approach

view this post on Zulip Bryan Gin-ge Chen (Jun 08 2020 at 20:30):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jun 08 2020 at 20:42):

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

view this post on Zulip 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

view this post on Zulip 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/

view this post on Zulip Kevin Buzzard (Jun 08 2020 at 20:44):

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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jun 08 2020 at 20:46):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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
Adding mathlib
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
Trying to download https://oleanstorage.azureedge.net/mathlib/470ccd328e15391cf328e0e006e13a06ff7d7b29.tar.xz to /home/buzzard/.mathlib/470ccd328e15391cf328e0e006e13a06ff7d7b29.tar.xz
100%|█████████████████████████████████████████████████████████████████████████████████████| 22.5M/22.5M [00:21<00:00, 1.07MiB/s]
Found mathlib oleans at https://oleanstorage.azureedge.net/mathlib/

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 08 2020 at 20:51):

rofl, working OK is 0 problems :D

view this post on Zulip 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