K-user mailing list

[soha hussein <husseinsoh AT gmail.com>]

Hi Traian,

It is now working, I am actually using a macbook. The problem was in the permission of 3 files, kompile, krun and checkjava script! the later was the one that i didn't check for permission, and was causing the problem. 

Also, I have one thing to tell you. There is something wrong in the latest build, I have a k file that is kompiling with the pervious k version and it isn't kompiling with the recent  build version. It is actually raising a javaexception, i'll attach it  below. Likely the stable version works and doesnt have the configuration variable bug so i'm using it. I am attaching the code and the exception raised in case you wanted to take a look at it.

Thank you Traian and Radu for your help,

Soha

Here is the code i was trying to run, 

require "modules/substitution.k"

module QWELFLOW

       imports SUBSTITUTION

        syntax Op ::= ";" |"||"

        syntax Flow ::= Known | Unknown

syntax Known ::= "here"

          |Flow Op Flow

|Id ">" Flow

syntax Unknown ::= "?"

|"??"

syntax Type ::= "unit" 

| "("FType "x" FType ")"

| "("Type "x" Type ")" [strict]

| "("Type")" [bracket]

| FType "->" FType

| FType ">>" FType

syntax FType ::= Type "{" Map "}"

syntax Exp ::=  Id

        | "<>" 

| "("Exp","Exp")" [strict]

| "fst" Exp [strict]

| "snd" Exp [strict]

| "lambda" Id ":" Type "." Exp [binder]

| "app" Exp Exp             [strict, left]

| "publish" Id ":" Type "." Exp [binder]

| "call" Exp "with" Exp [strict]

| "("Exp")" [bracket]

| Url

| Aux

syntax Aux ::= "union" Op "{" Map "}" "{" Map "}"

          | "uni" Op "{" Map "}"

    | "res"

    

syntax Url ::= Id "@" Id

syntax Pgm ::= Exp

syntax KResult ::= FType

configuration<T>

<k> $PGM:Pgm </k>

<fctxt> .Map </fctxt>

<serv> $SERV:Map </serv>

<w> "localhost" </w>

    </T>

syntax Exp ::= FType

//unit

rule <> => (unit {.Map})

//pair

rule (T1:FType , T2:FType) => (T1 x T2)

rule (((T1:Type) {M1:Map}):FType x (T2:Type {M2:Map}):FType) => (union || {M1} {M2}) ~>  ((T1 x T2){.Map}):FType  // this rule is causing the java exception

// defining parallel

    rule <k> union || {M1:Map} {M2:Map} => uni || {M2} ...</k>

    <fctxt> _=> M1 </fctxt>

rule <k> uni || {X|->F' M:Map} => uni || {M} ...</k>

    <fctxt> ... X|-> (F => F || F') ...</fctxt>

rule <k> uni || {X|->F M:Map} => uni || {M} ...</k>

    <fctxt> R:Map (.=> X|->F) </fctxt> when notBool (X in keys(R))

endmodule

and here is the exception

java.lang.RuntimeException: don't know how to maudify Cast

at org.kframework.backend.maude.MaudeFilter.visit(MaudeFilter.java:946)

at org.kframework.kil.Cast.accept(Cast.java:75)

at org.kframework.backend.maude.MaudeFilter.visit(MaudeFilter.java:646)

at org.kframework.backend.maude.MaudeFilter.visit(MaudeFilter.java:230)

at org.kframework.kil.KList.accept(KList.java:58)

at org.kframework.backend.maude.MaudeFilter.visit(MaudeFilter.java:512)

at org.kframework.kil.KApp.accept(KApp.java:143)

at org.kframework.backend.maude.MaudeFilter.visit(MaudeFilter.java:646)

at org.kframework.backend.maude.MaudeFilter.visit(MaudeFilter.java:518)

at org.kframework.kil.KSequence.accept(KSequence.java:54)

at org.kframework.backend.maude.MaudeFilter.visit(MaudeFilter.java:393)

at org.kframework.kil.Cell.accept(Cell.java:269)

at org.kframework.backend.maude.MaudeFilter.visit(MaudeFilter.java:479)

at org.kframework.kil.Rule.accept(Rule.java:73)

at org.kframework.backend.maude.MaudeFilter.visit(MaudeFilter.java:67)

at org.kframework.kil.Module.accept(Module.java:97)

at org.kframework.backend.maude.MaudeFilter.visit(MaudeFilter.java:40)

at org.kframework.kil.Definition.accept(Definition.java:116)

at org.kframework.backend.maude.MaudeBackend.run(MaudeBackend.java:31)

at org.kframework.backend.maude.KompileBackend.run(KompileBackend.java:58)

at org.kframework.kompile.KompileFrontEnd.genericCompile(KompileFrontEnd.java:310)

at org.kframework.kompile.KompileFrontEnd.kompile(KompileFrontEnd.java:262)

at org.kframework.main.Main.main(Main.java:49)

On Oct 30, 2013, at 3:16 PM, Traian Florin Șerbănuță <traian.serbanuta AT info.uaic.ro> wrote:

Hi Soha,

I assume you are running it on windows.

If so, it is prefferable to download the .tgz archive, as the zip archive does not preserve executable permissions.

one way to attempt to fix it is to make kompile and krun executable

does something like 

chmod a+x  kompile krun

work?

best wishes,

Traian

2013/10/30 soha hussein <husseinsoh AT gmail.com>

I do have the path configured to <my_dir>/k/bin, it is not working for the new download. Both installations (the one that is a month old and the one i downloaded today) have the same structure for the bin folder, the old one works the new one doesn't.

Could there be something wrong in the build?

- Soha

On Oct 30, 2013, at 10:35 AM, Radu Mereuta <headness13 AT gmail.com> wrote:

Hi Soha,

Yes, we had a small reconfiguration of the folder structure.

You will have to change the path to point to the new location of the /bin directory.

The old version would be in <your_dir>/k/dist/bin

The new location is in <your_dir>/k/bin

If you put that in your path, then it should work.

Radu

On Wed, Oct 30, 2013 at 8:43 AM, soha hussein <husseinsoh AT gmail.com> wrote:

Hi Radu, 

I was actually using the nightly version which i downloaded about a month ago, however i re-downloaded it again. This one looks different, i noticed different folder structure, and also I am unable to install this one. Precisely,  I have a problem running kompile. it says permission denied even when i try to run it as a super user, i checked the file permissions and they look okay to me. I tried on another machine still the same problem. I am wondering if i should be doing something other than replacing the old files with the new files with the same path configured? When i put the old version that i used to have, kompile runs but i have the old configuration variable problem i first posted. 

Thanks

Soha

On Oct 29, 2013, at 4:23 PM, Radu Mereuta <headness13 AT gmail.com> wrote:

Hi Soha,

Can you tell me what version are you using? We did have this problem at one point, but I managed to correct it in the last 2 or 3 weeks.

The fix should be available in the nightly version.

You can find the latest versions on the main page at http://www.kframework.org/ or if you want frequent updates, you can use the nightly branch from our GitHub repository.

If you have the latest version, and the error still persists, can you give me more details, because I couldn't reproduce the bug.

Radu

k-developer

On Tue, Oct 29, 2013 at 9:46 AM, Traian Florin Șerbănuță <traian.serbanuta AT info.uaic.ro> wrote:

Hi Soha,

It's good to hear from you!

Radu and Michael, could you please shed some light in these matters?  They seem mostly related to parsing, and it is conceivable that they should work as Soha suggests.

2013/10/26 soha hussein <husseinsoh AT gmail.com>

Hi,

I am Soha Hussein, I used to work in the JavaMOP team. Currently i'm working in Carnegie Mellon Qatar, and we are working on inferring some program features by typing for the purpose of enforcing some security properties. We used to work with Twelf, but Twelf has some limitations that doesn't allow us to manipulate the context of variables easily while typing. I suggested using K, and actually i've implemented our old language in it already and it is working pretty well. They liked it and now i'm in the step of adding more on our old typing system, I generally manipulate the maps which contains the context, 

I have two questions,

1. I want to populate the configuration while running, so i created the configuration variable $SRV and called krun with the -cSRV option. It works as long as I am not using something of sort Id. In fact i tried to run lambda_1 lesson_6 k program with the -cPGM option and the example in the reference manual  "-cPGM="lambda x . x", but again it complaining from x, if i tried to run , "1 + 1" it works fine. So the question is what is the problem with variables of sort Id.? How can i populate the configuration of things that has sort Id.?

I think that should be possible and the fact you cannot do it means it's a bug we should look into.  

2. My second question is about maps, if i tried to have something like that

syntax Exp ::= "{" Map"}", when i try to have a program that contains a map of this form, it doesn't compile. To go around this, i implement a List and then convert the List input into the Map, but this seems unnecessary and thought may be there is something better to do there.? 

I think that, again, this could be made to work, although, again,  you might need to  pass more options to kompile and krun.

Also I would appreciate if you gave me more information on Maps as well as their limitations.

We are in the process of redesigning Maps (and sets, bags, lists) to be more closely integrated with K, similarly to Integers and other builtin types.

In the meanwhile, one cannot subsort Maps to K and there might be some issues with mixing maps with concrete syntax, although I think this was already used in several projects, so there should be ways to circumvent this limitation.

The main issue is/was that it increases the number of ambiguities at parsing time.

best wishes,

Traian 

 

Thank you,

Soha

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user