K-user mailing list

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

actually, perhaps a better question: what does uname report? if our script is not correctly identifying that you are running on windows then it is likely adding the wrong directory.

On Tue, Feb 17, 2015 at 1: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