search

TryItOnline / tryitonline

The Try It Online family of online interpreters.
https://tryitonline.net
MIT License
539 stars 58 forks source link

Agda permission denied error #49

Closed ice1000 closed 5 years ago

ice1000 commented 6 years ago

See https://tio.run/##dVDNSsNAEL7vUwzUQ3LYPoBQIUKFIrZqfIFtujZbmt0knaWtIeBBRK968eqr5UXibH60pXiZ@ebjm29@xHIh6rrgA5jdPkxm0xA43yqMjUV@DQNeMmZSqUElqckRJrOj8srqCJXRR2RAlsNLq9ao9HCcWbFWuP9fcS8f17J1YZxD9fZFaaEMnBN@hqJ6@Syhev2AUCJQcYg7JYJbGdJcJXdTkchxBl5mDUpAv0c3Yj@XPozANQhws1ZmdTqlCIjq7Fum6YTgAHvOI/B7iyeZG9iR9a5nvI2NQNPsld0g7NzYhtenEm0wVnpJig65zTAXekN79MuUUAiYQ0RVUAK/oAOq929iCM4bGP2x0a9BTq9tw6hJjC0Eiu6I9krqcmkby1wylgilndZq8FKLIeZw1rw1jM22ee3RO8H36/oH

Simply import Agda.Builtin.Int will cause this error.

DennisMitchell commented 6 years ago

A lot of Agda's libraries are precompiled, but I seem to be missing a few. I tried to fix that, but I keep running into issues.

For now, I'll just copy the precompiled files to runner's home directory. That will make everything work, but it will be slow until I figure out precompilation.

ice1000 commented 6 years ago

Thank you!