Abella hangs after 'abella -o test.out -c test.thc'

[lambdacalculator]

(No input file given in command line.) Ctrl-C has no effect.

[chaudhuri]

Did you try Ctrl-D? Normally Ctrl-C is trapped in interactive mode (which is what happens if you have no input file).

[lambdacalculator]

OK, Ctrl-D ends the program. A couple of follow-ups, though:

• My first mistake in trying to produce a .thc file was to assume that the -c option was a switch with no arguments that produced a .thc file with the same prefix as the given .thm file. This was a fatal mistake because it clobbered my .thm file. Good thing I had a backup.
• My second mistake was not realizing that I was in interactive mode, since there was no prompt (as I had sent output to the .out file).

So, yes, my fault -- but I wonder if some safeguards might be put into place to prevent others from accidentally falling into the same trap. Some possibilities:

• If someone gives a combination of -o and no input file, then print a message to stdout (or stderr) indicating this before waiting for input. Alternatively, echo output both to the screen and the output file.
• Make -c an option with no arguments that always produces a .thc file. Alternatively, don't allow -c to overwrite a file unless it is a .thc file (similarly, perhaps, with -o and .out).

[chaudhuri]

The whole compilation mechanism will probably be overhauled/replaced soon once we get the reasoning level module system in a more usable form. Meanwhile I'll add a warning to stderr as you suggest for this combination of flags.

[lambdacalculator]

This is closed, but I just wanted to ask about the status. After not compiling with -c for a while, I accidentally clobbered my thm file again with abella -c myfile.thm, not remembering that -c requires an output filename. Above, I suggested that the -c option should not require a filename and always produce a .thc file, which is anyway what is expected by import. After losing another thm file, it seemed like a good time to bring this up again. (Again, I acknowledge that this was my oversight, but it should be harder to clobber files accidentally, IMHO.)

[chaudhuri]

My recommendation would be to let Abella take care of compiling for you. Abella automatically compiles any .thm files it needs when it sees an Import statement. There is very little reason for you to be running -c yourself nowadays.