seccomp.h not found

[MichaelStollBayreuth]

I'm trying to install loogle locally on my machine (running SuSE Tumbleweed). When I try lake exe loogle --help (after the lake exe cache get step), I get the error message

mstoll@xxx:~/lean4/loogle> lake exe loogle --help
info: [0/68] Compiling Seccomp c shim (.o)
error: > cc -c -o ./.lake/build/loogle_seccomp.o ./loogle_seccomp.c -I /home/mstoll/.elan/toolchains/leanprover--lean4---v4.5.0-rc1/include -fPIC
error: stderr:
./loogle_seccomp.c:3:10: fatal error: seccomp.h: No such file or directory
    3 | #include <seccomp.h>
      |          ^~~~~~~~~~~
compilation terminated.
error: external command `cc` exited with code 1

There is a file /usr/inlcude/linux/seccomp.h, but no /usr/include/seccomp.h. Commenting out line 3 of loogle_seccomp.c (which does the #include that the compiler is complaining about), I get loads of error messages pointing to missing declarations. Installing the libseccomp-devel package seems to provide a suitable seccomp.h file, but in the directory /usr/include/libseccomp/, which does not seem to be in the path searched for header files. Adding /libseccomp in suitable places helps.

Maybe at some point the presence (or whereabouts) of relevant header files can be checked (before they are needed to compile something), and a helpful message be printed if they are not there or not where they are expected?

[nomeata]

Thanks for trying out loogle!

The seccomp support is only really relevant when running loogle as a public service, else it’s just a distraction. I should make seccomp optional somehow in a way that users by default do not have to deal with it. Not sure how to implement such conditional compilation, though.

[femtomc]

Just a note that this also breaks the build process on MacOS (as far as I can tell).

However, I'm using cc = clang -- and I haven't tried explicitly using gcc. I can try a few more things and report back.

Ah -- bit more reading: https://en.wikipedia.org/wiki/Seccomp it seems like this hard dependency means it is not possible to build this on MacOS, without using virtualization to e.g. run the Linux kernel.

[nomeata]

For now, just comment out the two lines mentioning seccomp in the main file, and maybe in the lakefile.lean, and it should work.

[femtomc]

@nomeata Sorry, can you be a bit more specific -- I'm a bit new to the organizational aspects of Lean projects. (I can see lakefile.lean -- but the main file?)

[nomeata]

In Loogle.lean, there are these two lines

import Seccomp

and

    Seccomp.enable

Try removing both and see if you can build it.