Can't find a directory

[egunter]

bash-3.2$ pwd /Users/elsa/courses/cs422/sp2016/students/_class/_private/lectures/5 bash-3.2$ ls -d int-kompiled/ int-kompiled/ bash-3.2$ ls test.int test.int bash-3.2$ krun --directory "/Users/elsa/courses/cs422/sp2016/students/_class/_private/lectures/5/int-kompiled/" test.int [Error] Critical: Could not find a compiled definition. Use --directory to specify one. bash-3.2$

[egunter]

I have the same problem if Replace --directory by -d. If I leave out the directory specification and I krun test.int all works as expected.
---Elsa

[andreistefanescu]

Can you try this path /Users/elsa/courses/cs422/sp2016/students/_class/_private/lectures/5 (without int-kompiled)?

[egunter]

OK. That works.

What use is that if I have multiple ?-kompile directories in one place and want to specify which one? I don't understand the intent of this flag or the directory structure restrictions imposed by K. ---Elsa

On 2/9/16 1:14 PM, Andrei Stefanescu wrote:

Can you try this path |/Users/elsa/courses/cs422/sp2016/students/_class/_private/lectures/5| (without |int-kompiled|)?

— Reply to this email directly or view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_kframework_k_issues_2148-23issuecomment-2D182013153&d=BQMCaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=6HVnQqKkTakiuFWgzLrDZRn_aXW8wxBo_F_81lDI4NE&m=7J9zxZG1Z3OBqqpuhVEVtZr4Lh4ecQjE-vb7zVIt7Lw&s=H0KpNwfY3ggV8a--CBd70m-cZOQ4lkxTDqyZPaCdHCM&e=.

[grosu]

@andreistefanescu , @cos , @dwightguth : to me this looks like a bug. Can you please look into it?

@egunter: the idea is to allow multiple kompilations of the same language in the same folder, for example with different parameters; for example, one can be optimized for execution, another for search, another for verification. Each of them is stored in a different folder, and then you can refer to whichever you want depending on what you want to do. So to me it looks like you discovered a bug, where a default kompiled definition in the current directory is explicitly given through its absolute path and not recognized.

[daejunpark]

It is not a bug, but a feature. It works as follows: Suppose you kompile imp.k.

• By default, imp-kompiled directory is created in the directory imp.k resides in.
• When the option --directory X is provided, imp-kompiled is created in X (relative to the current directory if X is a relative path).

Now, when you run the semantics:

• By default, krun finds *-kompiled directory in the current directory.
• When the option --directory X is provided, krun finds *-kompiled directory in X.

When there are multiple *-kompiled directories in one place, krun will fail.

Rationale: We want to have the kompiled directory's name to be <language-name>-kompiled, so that krun automatically identifies the name of language (which is used as the file extension of programs, e.g., sum.imp) from the name of *-kompiled directory that it finds. Thus we do not allow users to provide their own name for *-kompiled directory.

[egunter]

This semantics is counter-intuitive and means you can not have a collection of files each building an approximation to a final language all in the same directory. If the name of the language must be prefixed to the -kompiled directory name and suffixed to the object files of that language, then why do you have the restriction that there can only be one *-kompiled directory in a given directory? The name can be learned and uniquely applied, thereby avoiding collisions. ---Elsa

On 2/10/16 12:31 AM, Daejun Park wrote:

It is not a bug, but a feature. It works as follows: Suppose you kompile |imp.k|.

• By default, |imp-kompiled| directory is created in the directory |imp.k| resides in.
• When the option |--directory X| is provided, |imp-kompiled| is created in |X| (relative to the current directory if |X| is a relative path).

Now, when you run the semantics:

• By default, |krun| finds |*-kompiled| directory in the current directory.
• When the option |--directory X| is provided, |krun| finds |*-kompiled| directory in |X|.

When there are multiple |*-kompiled| directories in one place, |krun| will fail.

Rationale: We want to have the kompiled directory's name to be |-kompiled|, so that |krun| automatically identifies the name of language (which is used as the file extension of programs, e.g., |sum.imp|) from the name of |-kompiled| directory that it finds. Thus we do not allow users to provide their own name for |-kompiled| directory.

— Reply to this email directly or view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_kframework_k_issues_2148-23issuecomment-2D182223417&d=BQMCaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=6HVnQqKkTakiuFWgzLrDZRn_aXW8wxBo_F_81lDI4NE&m=mTyr03FCWZwHeQrTrYLM_IgOS54WNIKqBNNQ4F29V8Q&s=4-MzbfFvCY2VVfwHyposvnQ0HBaFExGyqWdH_t5PbUQ&e=.

[grosu]

Now I remember, thanks @daejunpark.

you can not have a collection of files each building an approximation to a final language all in the same directory.

You can, but in that case you have to use options. Say you want to have imp1.k and imp2.k in the same folder, both defining approximations of the same language IMP (so main module is called IMP in both, and programs have extension .imp in both). Then kompile them as follows:

> kompile --directory imp1 --main-module IMP imp1.k
> kompile --directory imp2 --main-module IMP imp2.k

Now you got two folders, imp1 and imp2, each containing one kompiled definition. To krun programs, then mention again the --directory option:

> krun --directory imp1 ..\tests\sum.imp
> krun --directory imp2 ..\tests\sum.imp

If the name of the language must be prefixed to the -kompiled directory name and suffixed to the object files of that language,

That is not true and you should not rely on the particular names that kompile gives to the generated files/folders. For example, if you look into the imp1 and imp2 folders above, the generated folders are called imp1-kompiled and imp2-kompiled, resp., yet the programs all have the extension .imp.

why do you have the restriction that there can only be one *-kompiled directory in a given directory

We do not want people to rely on the particular names of the generated folders/files corresponding to a language model, nor to assume that the language model is all generated into one folder only. There were previous versions of K where we generated several files and folders at the top level. Also, different backends may generate completely different files. The more common case is when you generate different models for the same language, each kompiled with different options, for example one optimized for execution and another for speed.

Anyway, it was easier to just assume that each folder contains no more than one language model, and to refer to it you just have to provide the --directory option the path to that folder, without relying on any naming conventions for the generated files or folders. For example, if tomorrow we decide to change -kompiled to -temp, or to generate one such folder for each module in your definition, then you do not have to modify any of your scripts that kompile and krun programs.

BTW, this is a rarely used feature (proof being that I forgot the details).