Zulip Chat Archive

Stream: lean4

Topic: bitwise operations on `USize`


view this post on Zulip Calvin Lee (Feb 23 2021 at 19:16):

Are there any bitwise xor or not operations on the UInt types? I'm trying to write a fast hash for one of my types, but I can't find any way to do many bitwise operations

view this post on Zulip Andrew Kent (Feb 23 2021 at 20:21):

If you wanted some that don't yet exist in an expedient manner, you could add your own in the same way that is done here: https://github.com/leanprover/lean4/blob/master/src/Init/Data/UInt.lean#L248
The Float implementation also has some examples of declaring extern functions with C implementations where the definitions are opaque (you probably don't need to reason about the hash implementation, so that may work just fine).

view this post on Zulip Calvin Lee (Feb 23 2021 at 20:27):

Yeah, I was thinking about doing just that.
Would a PR for these changes be welcome?

view this post on Zulip Mario Carneiro (Feb 23 2021 at 21:30):

Unless there is a need for it to be in the core library, I think we should hold off on PRs for now

view this post on Zulip Mario Carneiro (Feb 23 2021 at 21:30):

I think extern functions can be added in user code, so there is no need for this ATM

view this post on Zulip Calvin Lee (Feb 23 2021 at 21:36):

hmm, how could I compile with a C program that would provide the behavior then? There is an issue with the base implementation for Nat in the core library, so that isn't really possible to link to

view this post on Zulip Calvin Lee (Feb 23 2021 at 21:58):

well I implemented it in my copy of lean as @Andrew Kent suggested until there's a better alternative, I'm submitting a pr so y'all can discuss, but I won't really be upset if it isn't merged https://github.com/leanprover/lean4/pull/321

view this post on Zulip Mario Carneiro (Feb 23 2021 at 23:01):

hmm, how could I compile with a C program that would provide the behavior then? There is an issue with the base implementation for Nat in the core library, so that isn't really possible to link to

I don't see the problem; the lean header defines a type like lean_nat_t, with some functions but not others, and then you can implement your own functions on this type and link to the header and link it in with a standard C compiler (which I think leanmake handles for you)

view this post on Zulip Andrew Kent (Feb 23 2021 at 23:02):

FWIW, you can open namespaces in any file, which makes it easy to "extend" functionality of things provided in Lean's core (and later if its added its easy to delete). I did this in a small project for some Float ops before they were added.

view this post on Zulip Mario Carneiro (Feb 23 2021 at 23:03):

I'm not saying that this isn't a useful addition, but it seems like something that will go in the (planned) mathlib prelude, since it isn't necessary for core to do its thing

view this post on Zulip Calvin Lee (Feb 23 2021 at 23:16):

@Mario Carneiro I mean that there is a C function called lean_nat_lxor it just had a bug so it wasn't usable

view this post on Zulip Mario Carneiro (Feb 23 2021 at 23:31):

oh, if there's a bug in existing lean 4 code then that sounds like a good PR

view this post on Zulip Mario Carneiro (Feb 23 2021 at 23:32):

(you should make it clearer in the PR that there is a bug fix in there, I missed that on first reading)

view this post on Zulip Calvin Lee (Feb 23 2021 at 23:41):

Indeed, but it also isn't currently used anywhere, so that's what this PR is adding

view this post on Zulip Zygimantas Straznickas (Feb 23 2021 at 23:54):

Relatedly, is there a proper way to make external definitions of dependencies available to the interpreter in the IDE? E.g. if I have a library that defines

@[extern c inline "#1 ^ #2"]
constant xor (a: UInt64) (b: UInt64) : UInt64

and, in a separate project open in vscode/emacs, I want to do

import MyLib
#eval xor 123 456

?

Currently I'm achieving this by building a hacked-together shared library and loading it through LD_PRELOAD when starting lean in-editor, but I feel there must be a less ugly way. I though plugins would achieve this but that didn't seem to work.

view this post on Zulip Mario Carneiro (Feb 23 2021 at 23:55):

mumble mumble nix

view this post on Zulip Mario Carneiro (Feb 23 2021 at 23:55):

@Sebastian Ullrich ?

view this post on Zulip Zygimantas Straznickas (Feb 24 2021 at 00:00):

(ideally without relinking lean on every library change :) ) but nix would work, thanks! the reason I didn't use it for my current project is I wanted to use some third-party deps, and they only had only been set up as leanpkg packages and not nix packages, and I was too lazy to fork/pr

view this post on Zulip Zygimantas Straznickas (Feb 24 2021 at 00:01):

I wonder if it's possible to write a nix rule to use a leanpkg package as a dep

view this post on Zulip Sebastian Ullrich (Feb 24 2021 at 07:46):

Yes, plugins are supposed to be the way to go here. No, we don't have support for automatically building & loading them in either the basic or the Nix build system right now. Though it certainly sounds easier for one of them...

view this post on Zulip Sebastian Ullrich (Feb 24 2021 at 07:47):

Zygimantas Straznickas said:

I wonder if it's possible to write a nix rule to use a leanpkg package as a dep

This was one of the open questions from my LT talk :)

view this post on Zulip Mario Carneiro (Feb 24 2021 at 08:02):

Is there any documentation or quickstart for this? I haven't the foggiest idea how to use all the compiler-styled features of lean 4

view this post on Zulip Sebastian Ullrich (Feb 24 2021 at 08:08):

No, this is still wholly unexplored. There is a single test making sure that --plugin works at all. https://github.com/leanprover/lean4/blob/master/tests/plugin/test_single.sh


Last updated: May 07 2021 at 13:21 UTC