Частота не меняется потому, что это X79. Решения есть, но пока они недостаточно хороши.
По поводу GPU power management — тут я подсказать не могу, HD3000 работает исправно.
Если исследовательский интерес действительно есть, присоединяйтесь к профильным сообществам вроде AppleLife и InsanelyMac и исследуйте на здоровье.
При использовании хорошего загрузчика, вроде Clover, для нормальной работы OS X на типичном современном железе (за исключением X79, у которого проблемы с поддержкой CPU power management, и Z87 по причине его новизны) нужна установка всего пары кекстов.
Как минимум, это FakeSMC.kext и драйверы для оборудования вроде встроенного Ethernet.
Наличие UEFI, кстати, для нормальных загрузчиков не обязательно, они эмулируют среду EFI для OS X. Более того, очень часто бывает, что в UEFI имеются ошибки и несовместимости с Apple EFI, отчего одна и та же система может лучше работать с legacy-загрузкой, чем с UEFI.
Есть небольшая проблема с поддержкой CPU power management в OS X на всех современных платах, кроме плат Gigabyte, которая решается либо патчем БИОСа, либо патчем кекста, либо установкой другого кекста взамен стандартного.
Я предпочитаю первый способ, для чего написал утилиту PMPatch.
Совсем забыть про BIOS получится пока только у обладателей оборудования с UEFI-совместимыми прошивками и отсутствием необходимости legacy-загрузки из MBR или с внешних устройств. Они могут отключить Compatibility Support Module совсем, после чего всем оборудованием вроде RAID/USB/SATA/Ethernet-контролеров начнут управлять драйверы UEFI, а не старые модули BIOS из CSM.
На некоторых платах можно выбрать, какая именно прошивка будет использоваться для вышеперечисленных контролеров, но на ноутбуках я такого пока не встречал.
UEFI GOP firmware есть «из коробки» на встроенных в SB/IB/Haswell графических картах Intel, а также на некоторых картах Nvidia 6xx и 7xx и ATI 7xxx. Вообще, тема UEFI достаточно интересная и там можно многое написать.
Если кому-то интересно, могу написать обзор формата файла EFI Capsule, типов используемых файлов и особенностях их модификации.
Заодно и пару полезных в хозяйстве патчей можно будет обсудить.
Не являюсь профессиональным математиком, чтобы судить, но на первый дилетансткий взгляд — отличная новая теория, берущаяся за основания математики с неожиданной стороны. Вот тут можно прочесть краткую историческую справку, чтобы понять, зачем она вообще нужна.
А вот тут — пояснение, что именно в ней нового и чем она отличается от ОТТ.
Вы верно говорите, что важен интерес человека к технологиям.
Только вот почему-то настойчиво проводите параллель между интересом к смартфонам/планшетам/электронным книгам/прочим гаджетам и интересам к технологиям.
Я интересуюсь технологиями, но мой интерес к гаджетам давно прошел.
Если новое устройство не решает никаких твоих задач, которых не решало бы старое, то покупать его — глупая и бессмысленная трата денег, независимо от того, что там в него добавили. И я не понимаю, почему для вас это странно.
А про технологии: вы слышали о протоколе FlexRay? А о сменяющем его RT Ethernet? А об ОСРВ AUTOSAR? О новых МК Infineon MCX1000? Есть множество очень интересных технологий, которые проходят мимо масс, но при этом они для причастных к ним людей не менее интересны.
По моему мнению, все эти гаджеты, планшеты, читалки, очки и часы — сильно переоценены. И делать хоть какие-то выводы по наличию оных у человека — это неправильно, вероятность ошибки слишком высока.
Я тот самый программист без смартфона.
Учусь в магистратуре TH Regensburg по специальности «Техническая информатика», через 3 недели последняя сессия.
Пишу на C для микроконтролеров, на С++/Qt для десктопа, разрабатываю дизайн плат в EagleCAD, патчу UEFI BIOS'ы, чиню электронику.
Погружен в дух профессии, слежу за новинками, читаю новости на 3 языках.
Не пользуюсь никакими сервисами Google, кроме синхронизации закладок в Chrome.
Пользуюсь простой звонилкой Nokia 6303i, с которой читаю только SMS.
Новости, почта, RSS, мессенджеры и уведомления достают за день так, что вечером дома я стараюсь вообще не включать ПК.
Если по вашему это все странно — я не знаю тогда. Иногда сигара — это просто сигара.
Выводимость можно описать как отношение формальной арифметики, и если формальная система Т может выражать отношения формальной арифметики, то она может выражать и выводимость. Да, отношение «высказывание S выводимо в T» посложнее, чем a+b=c, но принципиальной разницы между ними нет.
Прошу вас, прочтите Хофштадтера, там он вводит формальную систему (названную им Топографческой Теорией Чисел), в которой все манипуляции в ходе доказательства теоремы Гёделя можно отследить, просто считая палочки на бумаге.
Очень трудно описать гёделизацию простыми словами, но в английской вики у сообщества почти получилось.
Если доказательства на словах вас не устраивают, можете отследить работу системы доказательства теорем Nqthm, которую использовал Шанкар для доказательства теоремы Гёделя еще в 1986 году.
Пусть имеется формальная система Т, в которой можно выразить все утверждения формальной арифметики.
Если занумеровать каждую аксиому и каждое правило вывода, то сам процесс вывода какой либо теоремы (т.е. последовательного применения правил вывода к аксиомам и уже выведенным теоремам) можно рассматривать как манипуляцию с числами, т.е. сам вывод можно описать в терминах формальной арифметики.
Вот здесь и начинается проблема, т.к. можно построить автореферентное высказывание вида G = «G не выводима в формальной системе Т».
Если это высказывание выводимо, то его вывод является выводом не только G, но и высказывания not G = «G выводима в формальной системе Т», что делает формальную систему Т противоречивой. Если же вывод утверждения G не существует, то G — невыводимое в системе Т истинное утверждение (истинно оно потому, что оно утверждает свою невыводимость, и это действительно так), поэтому система Т — не полная.
На самом деле, теорему Гёделя можно доказывать не только построением «парадокса лжеца» в формальной системе, как это было сделано самим Гёделем, но и любым другим парадоксом, основанным на автореференции, например, парадоксом Берри.
Более того, существуют доказательства, не использующие автореференцию вообще, и основанные, к примеру, на теории вычислимости, но на пальцах я их пояснить уже не смогу.
Для понимания теоремы Гёделя очень советую прочесть книгу Д. Хофштадтера «Гёдель, Эшер, Бах — эта бесконечная гирлянда», там идея «странной петли», которая используется в доказательстве, пояснена на множестве простых примеров. Очень грубо и упрощенно теорему Гёделя о неполноте можно интерпретировать так: любой язык, достаточно мощный для того, чтобы быть собственным метаязыком (формальная арифметика — это язык именно такой мощности) либо не полон (содержит недоказуемые, т.е. не выводимые за конечное число шагов с помощью конечного числа правил вывода из конечного числа аксиом, истинные утверждения) либо противоречив (содержит доказательство как какой-либо гипотезы А, так и её отрицания not A).
Проблема именно в том, что язык становится для самого себя метаязыком, и на нем можно сформулировать автореферентную (ссылающуюся на саму себя) строчку вида G = «G — не теорема». Именно такая строчка и будет гёделевой для указанного языка. Парадоксальность утверждения «Это утверждение ложно» заметили еще древние греки, но его наличие не машает нам пользоваться естественным языком. Также и теорема Гёделя не сильно мешает использованию формальных систем.
Можно редактировать некоторые настройки AMI Aptio4 UEFI (на нем сейчас почти все современные десктопные платы) с помощью утилиты AMIBCP 4. Жаль только, что далеко не все.
Автору темы респект, отличный проект.
Я тоже сейчас неспеша занимаюсь темой патча UEFI: пишу поддержку новых БИОСов для плат на Z87 в PMPatch (это патчер для снятия защиты от записи с регистра 0xE2, которая не дает загружаться драйверу CPUPM из OS X).
Смотря в каком сегменте.
Если в обыкновенный ПК для дома — все перечисленные вполне конкуренты. Я не помню ни одного производителя плат на Z77, у которого был бы один шлак. Даже у ECS в тот раз получилось сделать что-то приличное.
Если брать оверклокеров, то Gigabyte, Asrock, MSI.
Если брать пользователей компактных систем, то Gigabyte, Asrock, MSI, Zotac.
А так при прочих равных для дома можно смело брать первую попавшуюся плату, разницу именно в надежности сейчас уже трудно заметить.
Регулярно получаю и оправляю посылки при помощи «постомата» Packstation. Покупаешь через интернет марку, заполняя при покупке адрес получателя, таможенные формуляры, если посылка должна проходить таможню, вес и размер посылки. Оплачиваешь марку через PayPal, печатаешь саму марку со штрихкодом и таможенные формы (если нужны), наклеиваешь все это на коробку. Подходишь к автомату, он сканирует штрих-код и предлагает открыть ящик 4 размеров на выбор. Кладешь посылку, закрываешь ящик, получаешь от автомата чек с номером для отслеживания, датой и временем принятия. Всё.
Получение тоже очень простое, тебе приходит СМС с кодом, приходишь к автомату, вводишь код и получаешь свою посылку. Такая система позволяет указать в качестве адреса получателя ближайший к тебе постомат, если паранойя не позволяет указать свой.
Если такую систему введут в России повсеместно — будет отлично, и не нужно ничего выдумывать дополнительно.
Сами ребята из BMW говорят, что технологии вроде Driver Assist или Drive-By-Wire с одной стороны улучшают автомобили и удешевляют их производство, но с другой лишают водителя кайфа от непосредственного управления. Причем люди, готовые за этот кайф платить, и являются основными покупателями дорогих и быстрых машин, поэтому практически все системы помощи водителю в них пока еще можно отключить.
Основным препятствием к производству полностью автоматических автомобилей является не инертность и недовольство водителей, а дороговизна соответствующей инфраструктуры, ведь автомобили должны общаться не только между собой, но и с электроникой внутри дорожного покрытия, станциями слежения за дорожной ситуацией и т.п. А на это все нужны деньги, которых не то, чтобы нет, но тратить их никто особенно не торопится.
Сейчас же основной вектор работ в области автоматизации вождения — стандартизация взаимодействия между разными авто и программными комплексами внутри каждого авто. В том числе и поэтому BMW отказываются от FlexRay в пользу RT Ethernet и от своих собственных наработок в пользу наработок проекта AUTOSAR.
Жаль только, что это все стремительно устаревает.
Некоторые из любителей новых технологий уже избавились от поддержки BIOS и загрузки через MBR полностью, и такой загрузчик у них работать уже не будет. Так что уже сейчас можно считать загрузку через MBR глубоким legacy.
Будущее — за UEFI. А там и загрузчик пишется в разы проще, и на ассемблере программировать уже не нужно, хоть и можно. Кому интересно почитать код и посмотреть на то, как нынче устроена загрузка — документация и исходные коды проекта TianoCore к вашим услугам.
И, судя по некоторым разговорам в кулуарах, в следующем году стендов производителей железа будет еще меньше, а те из них, кто останется, будут присутствовать только в бизнес-части, куда обычному посетителю выставки вход закрыт.
Уже сейчас стенды с китайскими USB-хабами и зарядниками занимают добрую половину павильона, а стендов Asus и Gigabyte нет вообще.
Да и людей, с которыми там хочется встретиться, приезжает все меньше и меньше с каждым годом. На Cebit 2012 было почти 40 оверклокеров и причастных к оверклокингу человек со всего мира, а на этой оверклокерское шоу устраивали только на стенде Asrock, и приехали хорошо если человек десять.
В общем, если так пойдет и дальше, то в следующем году вместо Cebit'а я поеду на Computex.
Смешно еще и то, что слова «сайт» и «онлайн» на кириллических языках для малознакомых с существующим интернетом людей звучат как очередной «абырвалг».
Как уже не раз говорилось, сама идея доменов на национальных языках — порочна. А новые «кириллические» домены со словами английского языка — это вообще ни в какие ворота уже.
По поводу GPU power management — тут я подсказать не могу, HD3000 работает исправно.
Если исследовательский интерес действительно есть, присоединяйтесь к профильным сообществам вроде AppleLife и InsanelyMac и исследуйте на здоровье.
При использовании хорошего загрузчика, вроде Clover, для нормальной работы OS X на типичном современном железе (за исключением X79, у которого проблемы с поддержкой CPU power management, и Z87 по причине его новизны) нужна установка всего пары кекстов.
Как минимум, это FakeSMC.kext и драйверы для оборудования вроде встроенного Ethernet.
Наличие UEFI, кстати, для нормальных загрузчиков не обязательно, они эмулируют среду EFI для OS X. Более того, очень часто бывает, что в UEFI имеются ошибки и несовместимости с Apple EFI, отчего одна и та же система может лучше работать с legacy-загрузкой, чем с UEFI.
Есть небольшая проблема с поддержкой CPU power management в OS X на всех современных платах, кроме плат Gigabyte, которая решается либо патчем БИОСа, либо патчем кекста, либо установкой другого кекста взамен стандартного.
Я предпочитаю первый способ, для чего написал утилиту PMPatch.
На некоторых платах можно выбрать, какая именно прошивка будет использоваться для вышеперечисленных контролеров, но на ноутбуках я такого пока не встречал.
UEFI GOP firmware есть «из коробки» на встроенных в SB/IB/Haswell графических картах Intel, а также на некоторых картах Nvidia 6xx и 7xx и ATI 7xxx. Вообще, тема UEFI достаточно интересная и там можно многое написать.
Если кому-то интересно, могу написать обзор формата файла EFI Capsule, типов используемых файлов и особенностях их модификации.
Заодно и пару полезных в хозяйстве патчей можно будет обсудить.
Вот тут можно прочесть краткую историческую справку, чтобы понять, зачем она вообще нужна.
А вот тут — пояснение, что именно в ней нового и чем она отличается от ОТТ.
Пришла на ум концовка песни Strange Charm:
«Is so God damn remarkable that I just sit in awe».
Только вот почему-то настойчиво проводите параллель между интересом к смартфонам/планшетам/электронным книгам/прочим гаджетам и интересам к технологиям.
Я интересуюсь технологиями, но мой интерес к гаджетам давно прошел.
Если новое устройство не решает никаких твоих задач, которых не решало бы старое, то покупать его — глупая и бессмысленная трата денег, независимо от того, что там в него добавили. И я не понимаю, почему для вас это странно.
А про технологии: вы слышали о протоколе FlexRay? А о сменяющем его RT Ethernet? А об ОСРВ AUTOSAR? О новых МК Infineon MCX1000? Есть множество очень интересных технологий, которые проходят мимо масс, но при этом они для причастных к ним людей не менее интересны.
По моему мнению, все эти гаджеты, планшеты, читалки, очки и часы — сильно переоценены. И делать хоть какие-то выводы по наличию оных у человека — это неправильно, вероятность ошибки слишком высока.
Учусь в магистратуре TH Regensburg по специальности «Техническая информатика», через 3 недели последняя сессия.
Пишу на C для микроконтролеров, на С++/Qt для десктопа, разрабатываю дизайн плат в EagleCAD, патчу UEFI BIOS'ы, чиню электронику.
Погружен в дух профессии, слежу за новинками, читаю новости на 3 языках.
Не пользуюсь никакими сервисами Google, кроме синхронизации закладок в Chrome.
Пользуюсь простой звонилкой Nokia 6303i, с которой читаю только SMS.
Новости, почта, RSS, мессенджеры и уведомления достают за день так, что вечером дома я стараюсь вообще не включать ПК.
Если по вашему это все странно — я не знаю тогда. Иногда сигара — это просто сигара.
Прошу вас, прочтите Хофштадтера, там он вводит формальную систему (названную им Топографческой Теорией Чисел), в которой все манипуляции в ходе доказательства теоремы Гёделя можно отследить, просто считая палочки на бумаге.
Очень трудно описать гёделизацию простыми словами, но в английской вики у сообщества почти получилось.
Если доказательства на словах вас не устраивают, можете отследить работу системы доказательства теорем Nqthm, которую использовал Шанкар для доказательства теоремы Гёделя еще в 1986 году.
Пусть имеется формальная система Т, в которой можно выразить все утверждения формальной арифметики.
Если занумеровать каждую аксиому и каждое правило вывода, то сам процесс вывода какой либо теоремы (т.е. последовательного применения правил вывода к аксиомам и уже выведенным теоремам) можно рассматривать как манипуляцию с числами, т.е. сам вывод можно описать в терминах формальной арифметики.
Вот здесь и начинается проблема, т.к. можно построить автореферентное высказывание вида G = «G не выводима в формальной системе Т».
Если это высказывание выводимо, то его вывод является выводом не только G, но и высказывания not G = «G выводима в формальной системе Т», что делает формальную систему Т противоречивой. Если же вывод утверждения G не существует, то G — невыводимое в системе Т истинное утверждение (истинно оно потому, что оно утверждает свою невыводимость, и это действительно так), поэтому система Т — не полная.
На самом деле, теорему Гёделя можно доказывать не только построением «парадокса лжеца» в формальной системе, как это было сделано самим Гёделем, но и любым другим парадоксом, основанным на автореференции, например, парадоксом Берри.
Более того, существуют доказательства, не использующие автореференцию вообще, и основанные, к примеру, на теории вычислимости, но на пальцах я их пояснить уже не смогу.
Проблема именно в том, что язык становится для самого себя метаязыком, и на нем можно сформулировать автореферентную (ссылающуюся на саму себя) строчку вида G = «G — не теорема». Именно такая строчка и будет гёделевой для указанного языка. Парадоксальность утверждения «Это утверждение ложно» заметили еще древние греки, но его наличие не машает нам пользоваться естественным языком. Также и теорема Гёделя не сильно мешает использованию формальных систем.
Автору темы респект, отличный проект.
Я тоже сейчас неспеша занимаюсь темой патча UEFI: пишу поддержку новых БИОСов для плат на Z87 в PMPatch (это патчер для снятия защиты от записи с регистра 0xE2, которая не дает загружаться драйверу CPUPM из OS X).
Если в обыкновенный ПК для дома — все перечисленные вполне конкуренты. Я не помню ни одного производителя плат на Z77, у которого был бы один шлак. Даже у ECS в тот раз получилось сделать что-то приличное.
Если брать оверклокеров, то Gigabyte, Asrock, MSI.
Если брать пользователей компактных систем, то Gigabyte, Asrock, MSI, Zotac.
А так при прочих равных для дома можно смело брать первую попавшуюся плату, разницу именно в надежности сейчас уже трудно заметить.
Спасибо за отчет, Дим.
Только слово «пропиетраных» поправь, уж больно страшное оно.
Получение тоже очень простое, тебе приходит СМС с кодом, приходишь к автомату, вводишь код и получаешь свою посылку. Такая система позволяет указать в качестве адреса получателя ближайший к тебе постомат, если паранойя не позволяет указать свой.
Если такую систему введут в России повсеместно — будет отлично, и не нужно ничего выдумывать дополнительно.
Основным препятствием к производству полностью автоматических автомобилей является не инертность и недовольство водителей, а дороговизна соответствующей инфраструктуры, ведь автомобили должны общаться не только между собой, но и с электроникой внутри дорожного покрытия, станциями слежения за дорожной ситуацией и т.п. А на это все нужны деньги, которых не то, чтобы нет, но тратить их никто особенно не торопится.
Сейчас же основной вектор работ в области автоматизации вождения — стандартизация взаимодействия между разными авто и программными комплексами внутри каждого авто. В том числе и поэтому BMW отказываются от FlexRay в пользу RT Ethernet и от своих собственных наработок в пользу наработок проекта AUTOSAR.
Некоторые из любителей новых технологий уже избавились от поддержки BIOS и загрузки через MBR полностью, и такой загрузчик у них работать уже не будет. Так что уже сейчас можно считать загрузку через MBR глубоким legacy.
Будущее — за UEFI. А там и загрузчик пишется в разы проще, и на ассемблере программировать уже не нужно, хоть и можно. Кому интересно почитать код и посмотреть на то, как нынче устроена загрузка — документация и исходные коды проекта TianoCore к вашим услугам.
Уже сейчас стенды с китайскими USB-хабами и зарядниками занимают добрую половину павильона, а стендов Asus и Gigabyte нет вообще.
Да и людей, с которыми там хочется встретиться, приезжает все меньше и меньше с каждым годом. На Cebit 2012 было почти 40 оверклокеров и причастных к оверклокингу человек со всего мира, а на этой оверклокерское шоу устраивали только на стенде Asrock, и приехали хорошо если человек десять.
В общем, если так пойдет и дальше, то в следующем году вместо Cebit'а я поеду на Computex.
Как уже не раз говорилось, сама идея доменов на национальных языках — порочна. А новые «кириллические» домены со словами английского языка — это вообще ни в какие ворота уже.