amelieled

Same question for #NAME.

Hi, I tried to compile c-semantics with docker file in my Ubuntu system. But failed. ``` Importing: Source(/home/user/mounted/semantics/common/options.k) Importing: Source(/home/user/mounted/semantics/common/settings.k) Importing: Source(/home/user/mounted/semantics/common/symloc.k) Importing: Source(/home/user/mounted/semantics/common/syntax.k) Importing: Source(/home/user/mounted/semantics/common/translation-unit.k) Importing: Source(/home/user/mounted/profiles/x86-gcc-limited-libc/semantics/c-settings.k) Importing: Source(/home/user/mounted/profiles/x86-gcc-limited-libc/semantics/c-extensions-translation.k)...

Yes, of course @gabrielhdt ! :) So until now, I've done: * parsing_tests/ (empty file and escaped identifier) * queries_tests/ (assert / assertnot / type / compute) * require_open_tests/ (require...

Problems: * Files which their name begins by a number (related to an issue so). * Maybe we can create the folder "theory_tests" or "examples_tests" (or remove redundancies) * I...

> I'll be picky, but I'd remove the suffix `_test`, because we know these are all tests, we're already in the `tests` folder... Yes, sure! Same thing for "description_blabla". >...

Very fun things can appear with this signature: `type -> type -> type`.

Just for your information, a file with almost 1 000 lines, isn't check quickly. It's really a problem.

Hi! I agree with you as well. But I'm also interested in learning, and perhaps helping, on this subject. Feel free to let me know what I can read/work to...

I've just targeted the problem a bit more: in fact, I've merged my 2 files above. The first one contains the following lines, and they are the problem, because when...

Yes I have the new mode of Gabriel but if I add "(load "lambdapi") in .emacs, I have the same problem. In fact, if I try to write a theorem...