bitwise operations on `USize`

Stream: lean4

[Calvin Lee]

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

[Andrew Kent]

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

[Calvin Lee]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Calvin Lee]

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

[Calvin Lee]

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

[Mario Carneiro]

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)

[Andrew Kent]

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.

[Mario Carneiro]

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

[Calvin Lee]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Calvin Lee]

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

[Zygimantas Straznickas]

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.

[Mario Carneiro]

mumble mumble nix

[Mario Carneiro]

@Sebastian Ullrich ?

[Zygimantas Straznickas]

(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

[Zygimantas Straznickas]

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

[Sebastian Ullrich]

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...

[Sebastian Ullrich]

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

[Mario Carneiro]

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

[Sebastian Ullrich]

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