search

cpitclaudel / cvc4.js

asm.js and WebAssembly ports of the CVC4 SMT solver
5 stars 0 forks source link

Compilation Instructions #1

Open yoni206 opened 6 years ago

yoni206 commented 6 years ago

I ran vagrant up in the vm/ directory, but I don't see any cvc4-js directory. Is there anything else that needs to be done?

cpitclaudel commented 6 years ago

What output did vagrant up produce?

yoni206 commented 6 years ago

Bringing machine 'default' up with 'virtualbox' provider... ==> default: Checking if box 'ubuntu/xenial32' is up to date... ==> default: A newer version of the box 'ubuntu/xenial32' is available! You currently ==> default: have version '20180726.0.0'. The latest is version '20180731.0.0'. Run ==> default: vagrant box update to update. ==> default: Clearing any previously set forwarded ports... ==> default: Clearing any previously set network interfaces... ==> default: Preparing network interfaces based on configuration... default: Adapter 1: nat ==> default: Forwarding ports... default: 22 (guest) => 2222 (host) (adapter 1) ==> default: Running 'pre-boot' VM customizations... ==> default: Booting VM... ==> default: Waiting for machine to boot. This may take a few minutes... default: SSH address: 127.0.0.1:2222 default: SSH username: vagrant default: SSH auth method: private key ==> default: Machine booted and ready! ==> default: Checking for guest additions in VM... ==> default: Mounting shared folders... default: /vagrant => /home/yoniz/git/CVC4/cvc4.js/vm ==> default: Machine already provisioned. Run vagrant provision or use the --provision ==> default: flag to force provisioning. Provisioners marked to run always will still run.

cpitclaudel commented 6 years ago

That's the second run; I need the log from the first one, which includes the output of the provisioning script

yoni206 commented 6 years ago

Thanks for helping! I destroyed the vm and did vagrant up again. I get the following output. It is different from the above, but I don't see any indication of the provision script. I also tried this with a new git-clone in a different directory, and also with --provision flag, but that provided the same result:

Bringing machine 'default' up with 'virtualbox' provider... ==> default: Importing base box 'ubuntu/xenial32'... ==> default: Matching MAC address for NAT networking... ==> default: Checking if box 'ubuntu/xenial32' is up to date... ==> default: A newer version of the box 'ubuntu/xenial32' is available! You currently ==> default: have version '20180726.0.0'. The latest is version '20180731.0.0'. Run ==> default: vagrant box update to update. ==> default: Setting the name of the VM: CVC4 ==> default: Clearing any previously set network interfaces... ==> default: Preparing network interfaces based on configuration... default: Adapter 1: nat ==> default: Forwarding ports... default: 22 (guest) => 2222 (host) (adapter 1) ==> default: Running 'pre-boot' VM customizations... ==> default: Booting VM... ==> default: Waiting for machine to boot. This may take a few minutes... default: SSH address: 127.0.0.1:2222 default: SSH username: vagrant default: SSH auth method: private key default: Warning: Remote connection disconnect. Retrying... default: default: Vagrant insecure key detected. Vagrant will automatically replace default: this with a newly generated keypair for better security. default: default: Inserting generated public key within guest... default: Removing insecure key from the guest if it's present... default: Key inserted! Disconnecting and reconnecting using new SSH key... ==> default: Machine booted and ready! ==> default: Checking for guest additions in VM... ==> default: Mounting shared folders... default: /vagrant => /home/yoniz/tmp/cvc4.js/vm

cpitclaudel commented 6 years ago

Oh! Of course. :man_facepalming: Sorry about this. That's because the provision line is commented out in the Vagrantfile…

Thanks for your patience :) Try the following: ssh into the VM with vagrant ssh, and then run the provision.sh script from there.

yoni206 commented 6 years ago

Thanks again for helping out with this :)

I did vagrant ssh and created there (in ~/) a file called provision.sh, to which I copy-pasted the contents of provision.sh of this repository. It indeed ran, and when I exited the vm, I saw that a cvc4-js was indeed created on my machine, under vm. Also, a CVC4 sub-folder was created under cvc4-js.

However - I did not find cvc4.js anywhere.

What should I do next?

cpitclaudel commented 6 years ago

It should be in the CVC4 subfolder; if it wasn't created, that likely means that something went wrong during the build; this time, you should have a more detailed log file created during provisioning, called "provision.log"

yoni206 commented 6 years ago

Yes, that is true - the build failed, the earliest failure in the log is in the installation of gmp: checking how to switch to text section... configure: error: Cannot determine text section directive ERROR:root:Configure step failed with non-zero return code: 1. Command line: ./configure --with-pic --disable-assembly --disable-fft --disable-shared at /vagrant/cvc4-js/gmp-6.1.2 make: *** No targets specified and no makefile found. Stop.

I googled this error, but didn't find anything helpful. Did you ever come across something like this in the build?

Complete log: provision.log

cpitclaudel commented 5 years ago

Sorry, I forgot to answer this. I haven't seen this issue before. Maybe it's due to your environment variables outside of the VM; my next step would be to try to understand how that test works in the configure script, and see if I can reproduce the issue separately.