catalin-hritcu

Toplevel input, characters 45-103:
Error: Illegal application (Non-functional construction): 
The expression "sprintf "<tr><td>%s</td><td>%b</td></tr>" name value" of type
 "(fix formatType (f : format) : Type :=
     match f with
     | [] => string
     | dir :: dirs =>
         match directiveType dir with
         | Some T => T -> formatType dirs
         | None => formatType dirs

catalin-hritcu

(* Reading:
http://www.cis.upenn.edu/~bcpierce/sf/ProofObjects.html
http://www.cis.upenn.edu/~bcpierce/sf/MoreInd.html
*)

Require Import Arith.

Print nat.
(*

catalin-hritcu

[97160.870886] ------------[ cut here ]------------
[97160.870893] WARNING: CPU: 2 PID: 15680 at drivers/gpu/drm/i915/intel_display.c:6890 hsw_enable_pc8+0x64b/0x6f0 [i915]()
[97160.870894] Power well on
[97160.870895] Modules linked in: ctr ccm fuse ecb uvcvideo btusb videobuf2_vmalloc videobuf2_memops uas videobuf2_core bluetooth videodev usb_storage media 6lowpan_iphc hid_generic snd_hda_codec_hdmi snd_hda_codec_realtek snd_hda_codec_generic joydev mousedev arc4 ext4 crc16 mbcache jbd2 iwlmvm mac80211 coretemp x86_pkg_temp_thermal intel_powerclamp iTCO_wdt iTCO_vendor_support kvm_intel kvm crct10dif_pclmul crc32_pclmul iwlwifi ghash_clmulni_intel aesni_intel aes_x86_64 lrw gf128mul glue_helper ablk_helper cryptd snd_hda_intel snd_hda_controller snd_hda_codec evdev i915 cfg80211 mac_hid psmouse serio_raw microcode rtsx_pci_ms snd_hwdep memstick thinkpad_acpi drm_kms_helper nvram snd_pcm led_class drm rfkill snd_timer hwmon wmi snd thermal e1000e intel_gtt tpm_tis i2c_algo_bit tpm soundcore battery
[97160.87

catalin-hritcu

[18 of 18] Compiling Main             ( mains/SafeMeld.hs, dist/build/safe-meld/safe-meld-tmp/Main.o )
Linking dist/build/safe-meld/safe-meld ...
Installing executable(s) in /home/hritcu/.cabal/bin
Installed safe-meld-0.0.2.1
make -C src clean install
make[1]: Entering directory '/home/hritcu/Penn/safe/git/src'
make -C lib/ArrayList clean
make[2]: Entering directory '/home/hritcu/Penn/safe/git/src/lib/ArrayList'
  File "/home/hritcu/Penn/safe/git/src/parse_deps.py", line 21
    print ' '.join([a, b, c, d, e])

catalin-hritcu

[hritcu@detained testing]$ aura -Akua

[sudo] password for hritcu: 
aura >>= Fetching package information...
aura >>= Comparing package versions...
aura >>= AUR Packages to upgrade:
aura-bin : 1.3.0.0-1 => 1.3.0.1-1
backintime : 1.0.34-4 => 1.0.36-3
backintime-gtk : 1.0.34-4 => 1.0.36-3
powerpill : 2014.8-1 => 2014.8.17-1

catalin-hritcu

[hritcu@detained src]$ opam switch
system  I system  System compiler (4.02.0)
4.02.1  C 4.02.1  Official 4.02.1 release
4.01.0  I 4.01.0  Official 4.01.0 release
3.12.1  I 3.12.1  Official 3.12.1 release
--     -- 3.11.2  Official 3.11.2 release
--     -- 4.00.0  Official 4.00.0 release
--     -- 4.00.1  Official 4.00.1 release
--     -- 4.02.0  Official 4.02.0 release
# 63 more patched or experimental compilers, use '--all' to show

catalin-hritcu

This is pdfTeX, Version 3.14159265-2.6-1.40.15 (TeX Live 2014/Arch Linux) (preloaded format=pdflatex 2015.3.5)  6 MAR 2015 20:27
entering extended mode
 restricted \write18 enabled.
 %&-line parsing enabled.
**main.tex
(./main.tex
LaTeX2e <2014/05/01>
Babel <3.9k> and hyphenation patterns for 79 languages loaded.
(./texdirectives.tex) (./llncs.cls
Document Class: llncs 2013/09/27 v2.18 

catalin-hritcu

unsat
label_1270
(error "line 30061 column 16: model is not available")
label_1271
(error "line 30063 column 16: model is not available")
label_1272
(error "line 30065 column 16: model is not available")
Done!
[quantifier_instances]    k!30037 :      1 :   1 : 2
[quantifier_instances]    k!30026 :      1 :   1 : 2

catalin-hritcu

(set-option :global-decls false)
(set-option :smt.mbqi false)
(set-option :smt.qi.profile true)
(declare-sort Ref)
(declare-fun Ref_constr_id (Ref) Int)

(declare-sort String)
(declare-fun String_constr_id (String) Int)

(declare-sort Kind)

catalin-hritcu

unsat
label_1270
(error "line 30061 column 16: model is not available")
label_1271
(error "line 30063 column 16: model is not available")
label_1272
(error "line 30065 column 16: model is not available")
Done!
[quantifier_instances]    k!30037 :      1 :   1 : 2
[quantifier_instances]    k!30026 :      1 :   1 : 2