search

uwdb / Cosette

Cosette is an automated SQL solver.
BSD 2-Clause "Simplified" License
666 stars 54 forks source link

Host `cosette' looks like a remote host, `docker' can only use the local host #3

Closed xuruiyang closed 7 years ago

xuruiyang commented 7 years ago

I run the command:

emacs /docker:cosette:/hott/UnivalentSemantics.v

as exactly as being written in your README file, and got the following error:

Host cosette' looks like a remote host,docker' can only use the local host

stechu commented 7 years ago

@xuruiyang does your Emacs have enable-remote-dir-locals enabled?

xuruiyang commented 7 years ago

Of course, it does I followed your instruction exactly.

stechu commented 7 years ago

@xuruiyang would you want to try it again?

I believe we have fixed the problems. It can build successfully on my machine.

you might need clean it up a bit first:

eg. run docker rm -f cosette first and redo the build process as listed in the readme.md

Please let us know if it still doesn't work on your side.

stechu commented 7 years ago

@xuruiyang we also updated the instructions so that you can pull the docker container from docker hub now.

xuruiyang commented 7 years ago

Thank you, I can pull the docker container successfully now.