Idris2 :load-file behaviour

[meraymond2]

In v1, :load-file would return a successful reply even if there were errors in the code. Now it returns an error, which is not in itself a problem, but I've run into two possible error cases so far.

1. It fails if a function is missing a case, and then if you call addMissing, it doesn't return that missing case. This can be tested with test/resources/test.idr.

client
  .loadFile("test/resources/test.idr")
  .then(console.log)
  .then(() => client.addMissing("getName", 7))
  .then(console.log)
  .catch((error) => {
    console.log("!!! " + error)
  })
  .then(() => {
    client.close()
    idrisProc.kill()
  })

{
  err: 'Error(s) building file test/resources/test.idr: test/resources/test.idr:7:1--8:1:Main.getName is not covering:\n' +
    '\tMissing cases:\n' +
    '\t($resolved1171 $resolved1169)',
  id: 1,
  ok: false,
  type: ':return'
}
{ id: 2, ok: true, missingClauses: '', type: ':return' }

2. Similar issue, but with addClause. I'm worried that the process is getting stuck on the error, and not loading the rest of the file correctly, because if you fix the missing case (test/resources/test-v2.idr), addClause works fine.

client
  .loadFile("test/resources/test.idr")
  .then(console.log)
  .then(() => client.addClause("f", 5))
  .then(console.log)
  .catch((error) => {
    console.log("!!! " + error)
  })
  .then(() => {
    client.close()
    idrisProc.kill()
  })

{
  err: 'Error(s) building file test/resources/test.idr: test/resources/test.idr:7:1--8:1:Main.getName is not covering:\n' +
    '\tMissing cases:\n' +
    '\t($resolved1171 $resolved1169)',
  id: 1,
  ok: false,
  type: ':return'
}
{
  initialClause: 'f not defined here',
  id: 2,
  ok: true,
  type: ':return'
}

[meraymond2]

I've checked my notes again, and for the first case, :add-missing returns nothing because it's not implemented yet, so that's not a bug. Possibly when it is implemented, it will work even if :load-file returns an error.

The second case is still a bug though, I need to raise an issue in the Idris repo.

[meraymond2]

I've raised an issue describing the breaking change.