K-user mailing list

[Dwight Guth <dwight.guth AT runtimeverification.com>]

Chucky: it should actually be doing this automatically. I suspect it's just not correctly detecting the OS. Again, can you tell me what `uname` reports?

On Tue, Feb 17, 2015 at 1:43 PM, Chucky Ellison <cme AT freefour.com> wrote:

Setting the paths did the trick!  I skipped over the "# IDE Setup" section, which is the part that says to add those three paths, because I didn't want to use K as an IDE (i just want to use it from the command line).  You may want to move this to another section.

It's a little strange that adding kompile to your path is optional, but adding those three 

<release>\lib\native\windows;

<release>\lib\native\windows64;

<release>\lib\native\64

are not.  And why all three?  Couldn't you just put them all in the same directory?

Oh well, at least it's running.  Thanks Brandon!

-Chucky

On Tue, Feb 17, 2015 at 2:20 PM, Moore, Brandon Michael <bmmoore AT illinois.edu> wrote:

The proper copy of sdf2table should be the one in
D:\prog\k\k-distribution\target\release\k\lib\native\windows

What directories do you have on your PATH?

Brandon

---

From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of Chucky Ellison [cme AT freefour.com]
Sent: Tuesday, February 17, 2015 9:04 AM
To: k-user AT cs.uiuc.edu; Traian Florin Serbanuta
Subject: [K-user] Fwd: installing the latest version of K

Resending this since it's been a while and I'm not entirely sure I was subscribed yet.

Any idea how to fix this so I can get K running?

Thanks!

-Chucky

---------- Forwarded message ----------
From: Chucky Ellison <cme AT freefour.com>
Date: Thu, Feb 12, 2015 at 11:20 AM
Subject: Re: [K-user] installing the latest version of K
To: Traian Florin Serbanuta <traian.serbanuta AT gmail.com>
Cc: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>

Okay I managed to `mvn package` everything, and that was successful.  Then I tried to `mvn install` (it seems to be required by the instructions, but not sure what any of this means).  It fails with an error (I attached the entire output).  It can't find "D:\prog\k\k-distribution\target\ktest-reports\summary.xml" (indeed, no such file exists).

Just in case `mvn install` was optional, I went ahead and tried to kompile a definition, and this is what I get:

$ kompile simple-typed-static.k

/d/prog/k/k-distribution/target/release/k/bin/../lib/k: line 3: ulimit: stack size: cannot modify limit: Invalid argument

java.io.IOException: Cannot run program "sdf2table.exe" (in directory "D:\prog\k\k-distribution\tutorial\2_languages\1_simple\2_typed\1_static\.kompile-2015-02-12-11-12-34-e6bc4c3d-d62a-4d4e-b8e8-5801c81cf49c\pgm"): CreateProcess error=2, The system cannot find the file specified

        at java.lang.ProcessBuilder.start(Unknown Source)

        at org.kframework.parser.utils.Sdf2Table.run_sdf2table(Sdf2Table.java:41)

        at org.kframework.parser.DefinitionLoader.parseDefinition(DefinitionLoader.java:172)

        at org.kframework.parser.DefinitionLoader.loadDefinition(DefinitionLoader.java:88)

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

        at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:87)

        at org.kframework.main.FrontEnd.main(FrontEnd.java:51)

        at org.kframework.main.Main.runApplication(Main.java:96)

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

Caused by: java.io.IOException: CreateProcess error=2, The system cannot find the file specified

        at java.lang.ProcessImpl.create(Native Method)

        at java.lang.ProcessImpl.<init>(Unknown Source)

        at java.lang.ProcessImpl.start(Unknown Source)

        ... 9 more

[Error] Critical: Could not copy

D:\prog\k\k-distribution\tutorial\2_languages\1_simple\2_typed\1_static\.kompile-2015-02-12-11-12-34-e6bc4c3d-d62a-4d4e-b8e8-5801c81cf49c\pgm\Program.tbl

to directory

D:\prog\k\k-distribution\tutorial\2_languages\1_simple\2_typed\1_static\simple-typed-static-kompiled\.

It looks like that program lives in both D:\prog\k\sdf-parser\target\sdf\bin and D:\prog\k\k-distribution\target\release\k\lib\native\windows, but it's not using those paths to find it I guess.

FWIW, I skipped the IDE setup part since I only want to run on the command line.

Help appreciated :)

(Incidentally, there's a typo in /src/README.md where it says "probabably").

-Chucky

On Thu, Feb 12, 2015 at 1:30 AM, Chucky Ellison <cme AT freefour.com> wrote:

Ah I see, I was following the /INSTALL.md instructions, when apparently I was supposed to follow the src/README.md instructions.  Since the /INSTALL.md file is in the base directory of the of the repository, you might want replace it with the contents of src/README.md, and put in your zips whatever install instructions you want.  Anyone who checks out is going to look first at /INSTALL.md.  Just a friendly suggestion :)  

I'll take another crack at the install tomorrow.  Thanks Traian!

-Chucky

On Thu, Feb 12, 2015 at 1:07 AM, Traian Florin Şerbănuţă <traian.serbanuta AT fmi.unibuc.ro> wrote:

Hi Chucky,

Welcome to K!... again :)

after you run mvn package in the base directory there should be a directory

   k-distribution/target/release/k

 

which is the K distribution 

Everything described in the documentation is based to that directory, and the scripts should be run from the bin directory there, too

Also, on Windows, I find that running the batch scripts works better for me, even though most of the time I run them from the cygwin environment.

best wishes,

Traian

2015-02-12 1:49 GMT+02:00 Chucky Ellison <cme AT freefour.com>:

So I'm trying to install the latest master of K (51c11bb93be74e68d15a5e63b1262428d15e90ce) on windows 7

$ java -version

java version "1.8.0_31"

Java(TM) SE Runtime Environment (build 1.8.0_31-b13)

Java HotSpot(TM) 64-Bit Server VM (build 25.31-b07, mixed mode)

I'm using the msys2 environment (it's like a cooler cygwin).

1) the instructions seem old; there is no k/bin directory.  I think it's now meant to be k-distribution\src\main\scripts\bin.  The same is true of the Simple example directory

2)

$ kompile simple-untyped.k

/d/prog/k/k-distribution/src/main/scripts/bin/../lib/k: line 3: ulimit: stack size: cannot modify limit: Invalid argument

Error: Could not find or load main class org.kframework.main.Main

I got a similar error when I tried running the example in v3.4.

It looks like there are two errors here.  One is about setting the stack size.  It fails, but the script continues.

$ ulimit -a

core file size          (blocks, -c) unlimited

data seg size           (kbytes, -d) unlimited

file size               (blocks, -f) unlimited

open files                      (-n) 256

pipe size            (512 bytes, -p) 8

stack size              (kbytes, -s) 2025

cpu time               (seconds, -t) unlimited

max user processes              (-u) 256

virtual memory          (kbytes, -v) unlimited

FWIW:

$ uname

MSYS_NT-6.1

When it goes to run java, It looks like it's setting the classpath to be

"$(dirname "$0")/java/*"

but my $(dirname "$0") is 

/d/prog/k/k-distribution/src/main/scripts/bin/../lib

and /d/prog/k/k-distribution/src/main/scripts/bin/../lib/java doesn't exist

Did I do something wrong?  What's going on?

Thanks!

-Chucky

_______________________________________________
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

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