proviola (python 2.7.3) barfs on some unicode characters

[palmskog]

Original report by Jason Gross (Bitbucket: jasongross9, ).

---

raceback (most recent call last):
  File "proviola/camera/camera.py", line 154, in <module>
    sys.exit(main())
  File "proviola/camera/camera.py", line 115, in main
    group = options.group)
  File "proviola/camera/camera.py", line 150, in make_film
    return reader.make_frames(prover = prover)
  File "/home/travis/build/JasonGross/HoTT/proviola/camera/coqdoc_reader.py", line 214, in make_frames
    scene = self._process_div(div)
  File "/home/travis/build/JasonGross/HoTT/proviola/camera/coqdoc_reader.py", line 196, in _process_div
    return self._process_doc(div)
  File "/home/travis/build/JasonGross/HoTT/proviola/camera/coqdoc_reader.py", line 165, in _process_doc
    child_scene = self._process_div(child)
  File "/home/travis/build/JasonGross/HoTT/proviola/camera/coqdoc_reader.py", line 196, in _process_div
    return self._process_doc(div)
  File "/home/travis/build/JasonGross/HoTT/proviola/camera/coqdoc_reader.py", line 165, in _process_doc
    child_scene = self._process_div(child)
  File "/home/travis/build/JasonGross/HoTT/proviola/camera/coqdoc_reader.py", line 194, in _process_div
    return self._process_code(div)
  File "/home/travis/build/JasonGross/HoTT/proviola/camera/coqdoc_reader.py", line 105, in _process_code
    commands = self.parse(t)
  File "/home/travis/build/JasonGross/HoTT/proviola/camera/CoqReader.py", line 91, in parse
    command = self.getWord(acc = acc)
  File "/home/travis/build/JasonGross/HoTT/proviola/camera/CoqReader.py", line 46, in getWord
    acc += char
UnicodeDecodeError: 'ascii' codec can't decode byte 0xc2 in position 23: ordinal not in range(128)

[palmskog]

Original comment by Jason Gross (Bitbucket: jasongross9, ).

---

I can't get proviola working with files generated by coqdoc --utf8, even after I do a bunch of manual unicodifying (https://bitbucket.org/JasonGross/proviola-source/branch/unicodify); pexpect doesn't know how to send unicode characters, and pexpect-u doesn't know how to handle the strange characters coqtop surrounds "Warning: Notation ~_ was already used in scope type_scope" with. Do you have any suggestions for getting the current version of proviola to work with coqdoc --utf8?

[palmskog]

Original comment by Jason Gross (Bitbucket: jasongross9, ).

---

I have a version of the .tar.gz code which works with the output of coqdoc --utf8 at JasonGross/proviola-source@9e6f1f1...master. At least, this is sufficient to integrate into the workflow of https://github.com/HoTT/HoTT in the proviola target of the Makefile. I'm happy to provide more feedback to get the latest version working with unicode, if there's anything in particular you want to know.

[palmskog]

Original comment by Carst Tankink (Bitbucket: Carst, GitHub: Carst).

---

Hi Jason,

Sorry for not getting back to you sooner. I didn't realize that pexpect cannot handle unicode. The problem with the tar.gz is that the parsing of HTML can be a bit wonky, but if it works for the HoTT files...

I will try and get a decent test-suite and fix during this week.

[palmskog]

Original comment by Jason Gross (Bitbucket: jasongross9, ).

---

Any update on this issue?

[palmskog]

Original comment by Carst Tankink (Bitbucket: Carst, GitHub: Carst).

---

Not yet, I was rather busy with preparing my defense and finding a new position.

However, I am now installed at Inria, and should be able to dedicate some time to this rather soon.