Usage advice?

[SamuelMarks]

> git clone --recurse-submodules https://github.com/lawcho/agda2c
agda2c - (master) > ./rpp-test.sh                   
Using PICO_SDK_FETCH_FROM_GIT from environment ('1')
Downloading Raspberry Pi Pico SDK
CMake Warning (dev) at /opt/homebrew/share/cmake/Modules/FetchContent.cmake:1953 (message):
  Calling FetchContent_Populate(pico_sdk) is deprecated, call
  FetchContent_MakeAvailable(pico_sdk) instead.  Policy CMP0169 can be set to
  OLD to allow FetchContent_Populate(pico_sdk) to be called directly for now,
  but the ability to call it with declared details will be removed completely
  in a future version.
Call Stack (most recent call first):
  pico_sdk_import.cmake:51 (FetchContent_Populate)
  CMakeLists.txt:6 (include)
This warning is for project developers.  Use -Wno-dev to suppress it.

PICO_SDK_PATH is agda2c/_build/_deps/pico_sdk-src
Defaulting platform (PICO_PLATFORM) to 'rp2040' since not specified.
Defaulting target board (PICO_BOARD) to 'pico' since not specified.
Using board configuration from agda2c/_build/_deps/pico_sdk-src/src/boards/include/boards/pico.h
Pico Platform (PICO_PLATFORM) is 'rp2040'.
-- Defaulting build type to 'Release' since not specified.
Defaulting compiler (PICO_COMPILER) to 'pico_arm_cortex_m0plus_gcc' since not specified.
Configuring toolchain based on PICO_COMPILER 'pico_arm_cortex_m0plus_gcc'
Defaulting PICO_GCC_TRIPLE to 'arm-none-eabi'
CMake Error at _deps/pico_sdk-src/cmake/preload/toolchains/util/find_compiler.cmake:29 (message):
  Compiler 'arm-none-eabi-gcc' not found, you can specify search path with
  "PICO_TOOLCHAIN_PATH".
Call Stack (most recent call first):
  _deps/pico_sdk-src/cmake/preload/toolchains/util/find_compiler.cmake:39 (pico_find_compiler)
  _deps/pico_sdk-src/cmake/preload/toolchains/util/pico_arm_gcc_common.cmake:25 (pico_find_compiler_with_triples)
  _deps/pico_sdk-src/cmake/preload/toolchains/pico_arm_cortex_m0plus_gcc.cmake:7 (include)
  /opt/homebrew/share/cmake/Modules/CMakeDetermineSystem.cmake:146 (include)
  CMakeLists.txt:9 (project)


CMake Error: CMake was unable to find a build program corresponding to "Unix Makefiles".  CMAKE_MAKE_PROGRAM is not set.  You probably need to select a different build tool.
CMake Error: CMAKE_C_COMPILER not set, after EnableLanguage
CMake Error: CMAKE_CXX_COMPILER not set, after EnableLanguage
-- Configuring incomplete, errors occurred!
agda2c - (master) > ls
_build		agda2c.dyn_hi	agda2c.hs	fptalk		UNLICENSE
agda-src	agda2c.dyn_o	agda2c.o	rpp-test.sh
agda2c		agda2c.hi	bubs		test.sh
agda2c - (master) > 
agda2c - (master) > ./test.sh 
_build/main.c:78:21: error: use of undeclared identifier 'build_AgdaziBuiltinziBoolziBoolzitrue'
   78 |         {return op0(build_AgdaziBuiltinziBoolziBoolzitrue);}
      |                     ^
_build/main.c:80:21: error: use of undeclared identifier 'build_AgdaziBuiltinziBoolziBoolzifalse'
   80 |         {return op0(build_AgdaziBuiltinziBoolziBoolzifalse);}}
      |                     ^
_build/main.c:92:21: error: use of undeclared identifier 'build_ForeignzmCziCorezitozmNat'
   92 |     app ( app ( op0(build_ForeignzmCziCorezitozmNat)
      |                     ^
_build/main.c:93:21: error: use of undeclared identifier 'build_ForeignzmCziCoreziRetzmTypeziuint16'
   93 |               , op0(build_ForeignzmCziCoreziRetzmTypeziuint16))
      |                     ^
_build/main.c:98:21: error: use of undeclared identifier 'build_ForeignzmCziCorezitozmNat'
   98 |     app ( app ( op0(build_ForeignzmCziCorezitozmNat)
      |                     ^
_build/main.c:99:21: error: use of undeclared identifier 'build_ForeignzmCziCoreziRetzmTypezibool'
   99 |               , op0(build_ForeignzmCziCoreziRetzmTypezibool))
      |                     ^
_build/main.c:107:21: error: use of undeclared identifier 'build_ForeignzmCziCorezifromzmNat'
  107 |     app ( app ( op0(build_ForeignzmCziCorezifromzmNat)
      |                     ^
_build/main.c:108:21: error: use of undeclared identifier 'build_ForeignzmCziCoreziRetzmTypeziuint16'
  108 |               , op0(build_ForeignzmCziCoreziRetzmTypeziuint16))
      |                     ^
_build/main.c:112:21: error: use of undeclared identifier 'build_ForeignzmCziCorezifromzmNat'
  112 |     app ( app ( op0(build_ForeignzmCziCorezifromzmNat)
      |                     ^
_build/main.c:113:21: error: use of undeclared identifier 'build_ForeignzmCziCoreziRetzmTypezibool'
  113 |               , op0(build_ForeignzmCziCoreziRetzmTypezibool))
      |                     ^
_build/main.c:117:21: error: use of undeclared identifier 'build_ForeignzmCziCorezifromzmNat'
  117 |     app ( app ( op0(build_ForeignzmCziCorezifromzmNat)
      |                     ^
_build/main.c:118:21: error: use of undeclared identifier 'build_ForeignzmCziCoreziRetzmTypezivoid'
  118 |               , op0(build_ForeignzmCziCoreziRetzmTypezivoid))
      |                     ^
12 errors generated.
Program crashed (exit not implemented yet)

Basically I want to specify the input file(s) and output directory, to produce C files from proved agda code.

Thanks for any and all tips

[lawcho]

You can find some algorithm & architecture documentation in my MSc thesis (mirror),
although that does not contain detailed advice on running the code in this repo.

The code in this repo was packaged for quick demos & live-coding,
rather than long-term reproducibility.

I tried to get this running again today, but couldn't get ./test.sh past the ./agda2c.hs line.
Stack failed at the link stage with usr/bin/ld.gold: error: cannot find -lgmp, which I don't want to debug.

Here is what I remember from two years ago, and reading through the scripts today:

• rpp-test.sh is set up to build code for the Raspbery Pi Pico

  • It you don't have a Pico board, this script is probably useless to you
  • rpp-test.sh tries to install the Pico SDK
  • It appears that the SDK's installer has bit-rotted (which seems to be causing your errors on rpp-test.sh)

• test.sh is set up for live-coding

  • It probably requires some heavy modification
  • e.g. it loads fptalk/Demo.agda which is empty
  • fptalk/Crib-Hello.agda is a more complete (& Pico-independent) example

• agda2c.hs emits C code that depends on the BUBS run-time system

  • It seems your agda2c.hs is running correctly, since it produced main.c
  • It seems the BUBS code (in bubs/) is detected OK, since you did not get errors for op0

• My best guess for your errors from test.sh is that:

  • test.sh ran agda2c.hs on an empty Demo.agda
  • agda2c.hs completed successfully
  • A nearly-empty main.c was produced
  • So Agda.Builtin.Bool never got compiled to C
  • So build_AgdaziBuiltinziBoolziBoolzitrue was not present at C-compile time
  • The run-time glue code always emitted by agda2c.hs requires build_AgdaziBuiltinziBoolziBoolzitrue to always be available
  • It wasn't, so GCC crashed

• I suspect the errors from test.sh will disappear if you add import Foreign-C.Core to your Agda source code