Problems running export to agda example

[GuilhermeMBP]

Hello, I am trying to run the example you have on your documentation: "Exporting to Agda". When I try to run the "SafetyProof.agda", I get this output:

Checking SafetyProof (/app/wind/agdaProof/SafetyProof.agda).
 Checking WindControllerSpec (/app/wind/agdaProof/WindControllerSpec.agda).
/app/wind/agdaProof/WindControllerSpec.agda:48,10-50,6
Error while running command 'vehicle validate --cache=/app/wind/verificationResult'
Input:

Output:

Error:
2024-06-07 11:27:45.358448: I external/local_tsl/tsl/cuda/cudart_stub.cc:32] Could not find cuda drivers on your machine, GPU will not be used.
2024-06-07 11:27:45.362000: I external/local_tsl/tsl/cuda/cudart_stub.cc:32] Could not find cuda drivers on your machine, GPU will not be used.
2024-06-07 11:27:45.409889: I tensorflow/core/platform/cpu_feature_guard.cc:210] This TensorFlow binary is optimized to use available CPU instructions in performance-critical operations.
To enable the following instructions: AVX2 FMA, in other operations, rebuild TensorFlow with the appropriate compiler flags.
2024-06-07 11:27:46.930869: W tensorflow/compiler/tf2tensorrt/utils/py_utils.cc:38] TF-TRT Warning: Could not find TensorRT
Unable to read the verification cache from file '/app/wind/verificationResult'
  error: /app/wind/verificationResult: openBinaryFile: inappropriate type (is a directory)

when checking that the expression
unquote
(checkSpecification
 (record { cache = "/app/wind/verificationResult" }))
has type (x : InputVector) → SafeInput x → SafeOutput x

from what I can tell, cache is not supposed to be a directory anymore?

I appreciate any help. Guilherme Pereira

[MatthewDaggitt]

Hi @GuilhermeMBP, sorry to hear that. Yup, I think it's not a directory any more, it's a single file. I'll try and fix that on Tuesday.

What version are you running and are you installing via Python or are you building from source?

[GuilhermeMBP]

I am using the latest 0.14.0 installed via Python, but I can build from source after that.

[MatthewDaggitt]

@GuilhermeMBP , v0.14.1 with the fix should now be live on pip.