## Stream: lean4

### Topic: bitwise operations on USize

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

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

#### Calvin Lee (Feb 23 2021 at 20:27):

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

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

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

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

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

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

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

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

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

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

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

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

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

#### Mario Carneiro (Feb 23 2021 at 23:55):

mumble mumble nix

#### Mario Carneiro (Feb 23 2021 at 23:55):

@Sebastian Ullrich ?

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

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

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

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

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

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