Debian Bug report logs - #498485
why: calls cpulimit with wrong arguments

Toggle useless messages

Message #5 received at submit@bugs.debian.org (full text, mbox, reply):

From: Timo Juhani Lindfors <timo.lindfors@iki.fi>

To: Debian Bug Tracking System <submit@bugs.debian.org>

Subject: why: calls cpulimit with wrong arguments

Date: Wed, 10 Sep 2008 14:50:21 +0300

Package: why
Version: 1.13-1
Severity: normal

calldp.ml calls cpulimit with

let cmd = sprintf "cpulimit %d %s > %s 2>&1" timeout cmd out in

but the cpulimit tool in debian expects different syntax:

$ cpulimit
Error: You must specify a target process
Usage: cpulimit TARGET [OPTIONS...]
   TARGET must be exactly one of these:
      -p, --pid=N        pid of the process
      -e, --exe=FILE     name of the executable program file
      -P, --path=PATH    absolute path name of the executable program file
   OPTIONS
      -l, --limit=N      percentage of cpu allowed from 0 to 100 (mandatory)
      -v, --verbose      show control statistics
      -z, --lazy         exit if there is no suitable target process, or if it dies
      -h, --help         display this help and exit


tools/cpulimit.c has an alternative cpulimit that has

fprintf(stderr,"usage: %s <time limit in seconds> <command>\n",argv[0]);

as the syntax.

Message #10 received at 498485@bugs.debian.org (full text, mbox, reply):

From: Mehdi Dogguy <Mehdi.Dogguy@pps.jussieu.fr>

To: Timo Juhani Lindfors <timo.lindfors@iki.fi>, 498485@bugs.debian.org

Subject: Re: Bug#498485: why: calls cpulimit with wrong arguments

Date: Wed, 10 Sep 2008 15:57:48 +0200

Timo Juhani Lindfors a écrit :
> Package: why
> Version: 1.13-1
> Severity: normal
> 
> calldp.ml calls cpulimit with
> 

From 2.01 (according to changelog[1]), Why started using its own version
of cpulimit (why-cpulimit) and doesn't depend anymore on cpulimit
(debian package).

Now Why uses only why-cpulimit.
So the bug disappeared with Why 2.01.

Try to get a newer version of Why !

[1] http://why.lri.fr/download/CHANGES

-- 
Mehdi Dogguy
http://www.pps.jussieu.fr/~dogguy/

Message #15 received at 498485@bugs.debian.org (full text, mbox, reply):

From: Mehdi Dogguy <Mehdi.Dogguy@pps.jussieu.fr>

To: Timo Juhani Lindfors <timo.lindfors@iki.fi>

Cc: 498485@bugs.debian.org

Subject: Re: Bug#498485: why: calls cpulimit with wrong arguments

Date: Wed, 10 Sep 2008 16:35:01 +0200

Timo Juhani Lindfors a écrit :
> Mehdi Dogguy <Mehdi.Dogguy@pps.jussieu.fr> writes:
>> Timo Juhani Lindfors a écrit :
>>> Package: why
>>> Version: 1.13-1
>>> Severity: normal
> 
> Whoops, I made a typo: I have why version "2.13-1" and not "1.13-1"

Ok. It was corrected in why ≥ 2.14.


-- 
Mehdi Dogguy
http://www.pps.jussieu.fr/~dogguy/

Message #20 received at 498485@bugs.debian.org (full text, mbox, reply):

From: Timo Juhani Lindfors <timo.lindfors@iki.fi>

To: Mehdi Dogguy <Mehdi.Dogguy@pps.jussieu.fr>

Cc: 498485@bugs.debian.org

Subject: Re: Bug#498485: why: calls cpulimit with wrong arguments

Date: Wed, 10 Sep 2008 17:08:26 +0300

Mehdi Dogguy <Mehdi.Dogguy@pps.jussieu.fr> writes:
> Timo Juhani Lindfors a écrit :
>> Package: why
>> Version: 1.13-1
>> Severity: normal
>> 
>> calldp.ml calls cpulimit with
>> 
>
>>From 2.01 (according to changelog[1]), Why started using its own version
> of cpulimit (why-cpulimit) and doesn't depend anymore on cpulimit
> (debian package).
>
> Now Why uses only why-cpulimit.
> So the bug disappeared with Why 2.01.
>
> Try to get a newer version of Why !

Whoops, I made a typo: I have why version "2.13-1" and not "1.13-1"
and I definitely can still see the bug:

Steps to reproduce:
0) cat > Lesson1.java <<EOF
public class Lesson1 {
    // jml2:
    // requires a != null && (\forall int i; 0 < i && i < a.length; a[i-1] <= a[i]);
    // krakatoa:
    //@ requires a != null && (\forall integer i; 0 < i && i < a.length ==>  a[i-1] <= a[i]);
    public int f0(int[] a) {
        return a[0];
    }
}
EOF
1) strace -o s -s4096 -f gwhy Lesson1.java
2) click ergo in the GUI

Expected results:
2) gwhy runs ergo

Actual results:
2) ergo is not started, strace reveals

852   execve("/usr/bin/cpulimit", ["cpulimit", "10", "ergo", "/tmp/gwhy9f0a8a_why.why"], [/* 46 vars */] <unfinished ...>

...

852   write(2, "Error: You must specify a target process\n"..., 41) = 41
852   write(2, "Usage: cpulimit TARGET [OPTIONS...]\n"..., 36) = 36
852   write(2, "   TARGET must be exactly one of these:\n"..., 40) = 40
852   write(2, "      -p, --pid=N        pid of the process\n"..., 44) = 44
852   write(2, "      -e, --exe=FILE     name of the executable program file\n"..., 61) = 61
852   write(2, "      -P, --path=PATH    absolute path name of the executable program file\n"..., 75) = 75
852   write(2, "   OPTIONS\n"..., 11)   = 11
852   write(2, "      -l, --limit=N      percentage of cpu allowed from 0 to 100 (mandatory)\n"..., 77) = 77
852   write(2, "      -v, --verbose      show control statistics\n"..., 49) = 49
852   write(2, "      -z, --lazy         exit if there is no suitable target process, or if it dies\n"..., 84) = 84
852   write(2, "      -h, --help         display this help and exit\n"..., 52) = 52

Please let me know if you are unable to reproduce this bug with 2.13-1.


best regards,
Timo Lindfors

Message #27 received at 498485@bugs.debian.org (full text, mbox, reply):

From: Timo Juhani Lindfors <timo.lindfors@iki.fi>

To: Mehdi Dogguy <Mehdi.Dogguy@pps.jussieu.fr>

Cc: 498485@bugs.debian.org

Subject: Re: Bug#498485: why: calls cpulimit with wrong arguments

Date: Wed, 10 Sep 2008 18:01:38 +0300

Mehdi Dogguy <Mehdi.Dogguy@pps.jussieu.fr> writes:
> Ok. It was corrected in why ≥ 2.14.

Ok, it is probably too late to correct this for debian lenny? At the
moment it is not possible to launch any provers from gwhy GUI because
of the issue :-(

Message #32 received at 498485@bugs.debian.org (full text, mbox, reply):

From: Mehdi Dogguy <Mehdi.Dogguy@pps.jussieu.fr>

To: Timo Juhani Lindfors <timo.lindfors@iki.fi>

Cc: jcristau@debian.org, 498485@bugs.debian.org

Subject: Re: Bug#498485: why: calls cpulimit with wrong arguments

Date: Wed, 10 Sep 2008 17:33:24 +0200

Timo Juhani Lindfors a écrit :
> Mehdi Dogguy <Mehdi.Dogguy@pps.jussieu.fr> writes:
>> Ok. It was corrected in why ≥ 2.14.
> 
> Ok, it is probably too late to correct this for debian lenny? At the
> moment it is not possible to launch any provers from gwhy GUI because
> of the issue :-(

You just have to write a wrapper for cpulimit to solve your problem.
I don't think it's possible to correct it in lenny ... Can you confirm
that Julien ? What can we do ?

-- 
Mehdi Dogguy
http://www.pps.jussieu.fr/~dogguy/

Message #37 received at 498485@bugs.debian.org (full text, mbox, reply):

From: Julien Cristau <jcristau@debian.org>

To: Mehdi Dogguy <Mehdi.Dogguy@pps.jussieu.fr>

Cc: Timo Juhani Lindfors <timo.lindfors@iki.fi>, 498485@bugs.debian.org

Subject: Re: Bug#498485: why: calls cpulimit with wrong arguments

Date: Wed, 10 Sep 2008 16:43:36 +0100

On Wed, Sep 10, 2008 at 17:33:24 +0200, Mehdi Dogguy wrote:

> Timo Juhani Lindfors a écrit :
> > Mehdi Dogguy <Mehdi.Dogguy@pps.jussieu.fr> writes:
> >> Ok. It was corrected in why ≥ 2.14.
> > 
> > Ok, it is probably too late to correct this for debian lenny? At the
> > moment it is not possible to launch any provers from gwhy GUI because
> > of the issue :-(
> 
> You just have to write a wrapper for cpulimit to solve your problem.
> I don't think it's possible to correct it in lenny ... Can you confirm
> that Julien ? What can we do ?
> 
Install why's cpulimit in /usr/lib/why/, and teach the program to
execute that instead of the one in $PATH?  If the patch is not too big,
fixing in lenny would probably be possible.

Cheers,
Julien

Message #42 received at 498485-close@bugs.debian.org (full text, mbox, reply):

From: Julien Cristau <jcristau@debian.org>

To: 498485-close@bugs.debian.org

Subject: Bug#498485: fixed in why 2.13-2

Date: Wed, 17 Sep 2008 21:17:31 +0000

Source: why
Source-Version: 2.13-2

We believe that the bug you reported is fixed in the latest version of
why, which is due to be installed in the Debian FTP archive:

why_2.13-2.diff.gz
  to pool/main/w/why/why_2.13-2.diff.gz
why_2.13-2.dsc
  to pool/main/w/why/why_2.13-2.dsc
why_2.13-2_i386.deb
  to pool/main/w/why/why_2.13-2_i386.deb



A summary of the changes between this version and the previous one is
attached.

Thank you for reporting the bug, which will now be closed.  If you
have further comments please address them to 498485@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.

Debian distribution maintenance software
pp.
Julien Cristau <jcristau@debian.org> (supplier of updated why package)

(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmaster@debian.org)


-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Format: 1.8
Date: Wed, 17 Sep 2008 21:45:11 +0200
Source: why
Binary: why
Architecture: source i386
Version: 2.13-2
Distribution: unstable
Urgency: low
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Julien Cristau <jcristau@debian.org>
Description: 
 why        - A software verification tool
Closes: 498485 499140
Changes: 
 why (2.13-2) unstable; urgency=low
 .
   [ Mehdi Dogguy ]
   * Using why-cpulimit instead of cpulimit Debian package, closes: 498485.
   * Renaming 'dp' into 'why-dp', closes: #499140.
   * Remove unnecessary dependency : cpulimit.
Checksums-Sha1: 
 61a08bf7faf15fcba4c953d17d3a8aa662fc6f73 1363 why_2.13-2.dsc
 65a8bc74d1c16f651af1fbdf4593da3035c2391b 5843 why_2.13-2.diff.gz
 af039d8b8a778e0f76c2d5b7d91c4879c34d45af 4614976 why_2.13-2_i386.deb
Checksums-Sha256: 
 e1c24bbeec4b8786b316a5a36576bcf97b6e255b7c346f61202b6dfae827d480 1363 why_2.13-2.dsc
 4db32ec80463244ea246c5ec393fbf442f7836f4cacdfde9dddd0214c91430aa 5843 why_2.13-2.diff.gz
 783ccc63de50e031e2965cee06d0411e986c10caf5efcc1b3599251195698ad8 4614976 why_2.13-2_i386.deb
Files: 
 889ee6bad804a548d1b093f5f04cd131 1363 math optional why_2.13-2.dsc
 877a9b50d152efab078dbd6300fbfd85 5843 math optional why_2.13-2.diff.gz
 2b17c32b0d96faf027d98066425d0977 4614976 math optional why_2.13-2_i386.deb

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.9 (GNU/Linux)

iEYEARECAAYFAkjRZSoACgkQmEvTgKxfcAwCzQCeJ+/8+dl0RcZfx1brF5LF9iD5
oaoAni44fUQaiDwqVbtW84DI9tyVVXmm
=Sfub
-----END PGP SIGNATURE-----

Send a report that this bug log contains spam.