Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Error creating temp file #2

Open
Kevinpgalligan opened this issue Dec 26, 2019 · 8 comments
Open

Error creating temp file #2

Kevinpgalligan opened this issue Dec 26, 2019 · 8 comments

Comments

@Kevinpgalligan
Copy link

Kevinpgalligan commented Dec 26, 2019

Hi,

I tried to run one of the example commands in SLIME -- (solve '(and (or a b) (or a !b c)) :minisat) -- after successfully installing cl-sat.minisat, but encountered the following error:

Subprocess with command "mktemp --tmpdir='/tmp/'  cnf.XXXXXXX"
 exited with error code 1
   [Condition of type UIOP/RUN-PROGRAM:SUBPROCESS-ERROR]

Restarts:
 0: [CONTINUE] IGNORE-ERROR-STATUS
 1: [RETRY] Retry SLIME REPL evaluation request.
 2: [*ABORT] Return to SLIME's top level.
 3: [ABORT] abort thread (#<THREAD "repl-thread" RUNNING {1002F283E3}>)

Backtrace:
  0: (UIOP/RUN-PROGRAM::%CHECK-RESULT 1 :COMMAND "mktemp --tmpdir='/tmp/'  cnf.XXXXXXX" :PROCESS NIL :IGNORE-ERROR-STATUS NIL)
  1: (UIOP/RUN-PROGRAM::%USE-SYSTEM "mktemp --tmpdir='/tmp/'  cnf.XXXXXXX" :OUTPUT (:STRING :STRIPPED T))
  2: ((:METHOD SOLVE (SAT-INSTANCE T)) #<SAT-INSTANCE {1003DF3603}> :MINISAT) [fast-method]
  3: (SB-INT:SIMPLE-EVAL-IN-LEXENV (SOLVE (QUOTE (AND # #)) :MINISAT) #<NULL-LEXENV>)
  4: (EVAL (SOLVE (QUOTE (AND # #)) :MINISAT))

Same error if I run the command through the REPL: (uiop:run-program "mktemp --tmpdir='/tmp/' cnf.XXXXXXX"), which indicates it's not a problem with cl-sat specifically.

If I try to run the command myself from the terminal -- mktemp --tmpdir='/tmp/' cnf.XXXXXXX -- it works fine.

If I run the command through the SBCL interpreter, it succeeds: (uiop:run-program "mktemp --tmpdir='/tmp/' cnf.XXXXXXX")

Any idea what might be the issue? Thanks!

@Kevinpgalligan
Copy link
Author

Aaaand if I run the command through the SBCL interpreter, it works just fine. So this seems to be an issue with my REPL / Portacle. Closing this.

@guicho271828
Copy link
Collaborator

Still curious to see where it's happening. I don't know what portacle is actually doing, but is it perhaps using a container based infrastructure like docker? Then it's possible that /tmp/ is not mounted in that container

@Kevinpgalligan
Copy link
Author

Didn't think of that, good shout. I'll experiment when I'm at home again. If it turns out to be a missing tmp folder in the Portacle environment, I might send a pull request here to quietly create a tmp folder in the with-tmp utility function, if that makes sense. It would make my life easier, at least.

@Kevinpgalligan
Copy link
Author

Kevinpgalligan commented Dec 28, 2019

Right, I figured out what's wrong. Portacle is overriding the mktemp command. See here for details: portacle/portacle#129

I suggest changing the call to the mktemp command to avoid the --tmpdir argument, since this approach seems to be more portable. Pull request incoming, let me know if you agree.

@Kevinpgalligan
Copy link
Author

Kevinpgalligan commented Dec 29, 2019

I've prepared a fix (see: https://github.com/Kevinpgalligan/cl-sat), and the new version of with-temp works in Portacle, but I've run into some issues while trying to test cl-sat:solve.

Here's what I run, with output:

CL-USER> (asdf:system-source-directory :cl-sat)
#P"/home/kevin/portacle/all/quicklisp/local-projects/cl-sat/"
CL-USER> (asdf:system-source-directory :cl-sat.minisat)
#P"/home/kevin/portacle/all/quicklisp/dists/quicklisp/software/cl-sat.minisat-20190202-git/"
CL-USER> (cl-sat:solve '(and (or a b) (or a !b c)) :minisat)
; cd /tmp/minisat.XXj2S3KK; /home/kevin/portacle/all/quicklisp/dists/quicklisp/software/cl-sat.minisat-20190202-git/minisat/build/release/bin/minisat  /tmp/cnf.Xtb8vHH resultWARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
|                                                                             |
|  Number of variables:             6                                         |
|  Number of clauses:               2                                         |
|  Parse time:                   0.00 s                                       |
|  Eliminated clauses:           0.00 Mb                                      |
|  Simplification time:          0.00 s                                       |
|                                                                             |
============================[ Search Statistics ]==============================
| Conflicts |          ORIGINAL         |          LEARNT          | Progress |
|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
===============================================================================
===============================================================================
restarts              : 1
conflicts             : 0              (0 /sec)
decisions             : 1              (0.00 % random) (3425 /sec)
propagations          : 3              (10274 /sec)
conflict literals     : 0              (-nan % deleted)
Memory used           : 6.02 MB
CPU time              : 0.000292 s

SATISFIABLE
[this is where the output stops]

It errors out before printing the variables:

The function CL-SAT.MINISAT::SAT-INSTANCE-VARIABLES is undefined.
   [Condition of type UNDEFINED-FUNCTION]

Restarts:
 0: [CONTINUE] Retry calling CL-SAT.MINISAT::SAT-INSTANCE-VARIABLES.
 1: [USE-VALUE] Call specified function.
 2: [RETURN-VALUE] Return specified values.
 3: [RETURN-NOTHING] Return zero values.
 4: [RETRY] Retry SLIME REPL evaluation request.
 5: [*ABORT] Return to SLIME's top level.
 --more--

Backtrace:
  0: ("undefined function" #<CL-SAT:SAT-INSTANCE {10020A0B63}>)
  1: ((:METHOD CL-SAT:SOLVE (PATHNAME (EQL :MINISAT))) #P"/tmp/cnf.Xtb8vHH" #<unused argument>) [fast-method]
  2: ((:METHOD CL-SAT:SOLVE (CL-SAT:SAT-INSTANCE T)) #<CL-SAT:SAT-INSTANCE {10020A0B63}> :MINISAT) [fast-method]
  3: (SB-INT:SIMPLE-EVAL-IN-LEXENV (CL-SAT:SOLVE (QUOTE (AND # #)) :MINISAT) #<NULL-LEXENV>)
  4: (EVAL (CL-SAT:SOLVE (QUOTE (AND # #)) :MINISAT))
 --more--

Any idea what's wrong? Also, are there any other ways that I should test my change, besides running solve within Portacle? I'm rather new to Common Lisp, so help would be appreciated.

Thanks!

@Kevinpgalligan
Copy link
Author

It just occurred to me that the version of cl-sat.mini I've pulled using quicklisp may be incompatible with the most recent version of cl-sat, I'll try again tomorrow with the most up-to-date cl-sat.mini.

@guicho271828
Copy link
Collaborator

yes, sat-instance-variables function is gone in the latest. I guess you have an old version of the code somewhere in the system (e.g. local-projects/ ) and mixing them up.

@Kevinpgalligan
Copy link
Author

Kevinpgalligan commented Dec 29, 2019

Confirmed that it works in Portacle now. Sent a pull request (see above). I know it's just addressing my specific case and still won't work on all systems, so I understand if you want to do something more thorough here.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants